A special focus of the Deduktionstreffen is on young researchers and students, who are particularly encouraged to present their ongoing research projects to a wider audience. Another goal of the meeting is to stimulate networking effects and to foster collaborative research projects.
We welcome contributions on all theoretical, experimental and application aspects of deduction. Accepted abstracts are first presented in a 15 minute teaser talk and then discussed next to a poster (maximal size: A0 portrait).
The Deduktionstreffen will also host the annual general meeting of the members of FGDedSys.
Deduktionstreffen 2018 is associated with the Luxembourg Logic for AI Summit (LuxLogAI), which brings together several renowned conferences and events, including RuleML+RR 2018, DecisionCAMP 2018, the Reasoning Web Summer School (RW 2018), the Global Conference on Artificial Intelligence (GCAI 2018) and the MIREL 2018 workshop.
Submission is open to everybody interested in deduction systems. Particularly encouraged are submissions that address one or several topics of the overall focus theme of the LuxLogAI Summit: Methods and Tools for Responsible AI.
Dennis Müller, Florian Rabe and Michael Kohlhase: Mathematical Interface Theories for System Integration
Jonas Betzendahl: Proof Recovery for the IMPS system
Marco Träger: Automatic generation of Invariants for Concurrent Programs
Dennis Peuter and Viorica Sofronie-Stokkermans: On Inductive Verification and Synthesis
Phillip Lippe and Stephan Schulz: Deep Reasoning - Hardware Accelerated Artificial Intelligence
Sophie Siebert and Frieder Stolzenburg: CoRg: Commonsense Reasoning Using a Theorem Prover and Machine Learning
10:30 Poster Session and Coffee Break
11:00 Session 2
Invited Talk by Pascal Fontaine: Quantifier handling in SMT
Stephan Schulz: Herbrand's Revenge - SAT Solving for First-Order Theorem Proving
Fred Freitas: A Roadmap to Gradually Compare and Benchmarking Description Logic Calculi
12:30 Lunch Break
14:00 Session 3
Mathias Fleury: IsaSAT, a verified SAT Solver using Isabelle/HOL
Abhik Pal, Benedikt Stock, Marco David, Deepak Aryal, Jonas Bayer, Bogdan Ciurezu, Yiping Deng, Prabaht Devkota, Simon Dubischar, Malte Sophian Hassler, Yufei Liu and Maria Antonia Oprea: Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Maximilian P. L. Haslbeck and Simon Wimmer: Competitive Proving for Fun
David Fuenmayor: Computational Hermeneutics: Using Automated Reasoning for the Logical Analysis of Natural-Language Arguments
Lukas Grätz: Leibniz on Reasoning about Impossible Concepts
15:15 Poster Session and Coffee Break
16:00 Session 4
Invited Talk by Cynthia Kop: Wanda: a higher-order termination tool