CADE-28: THE 28TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

A
Aaronson, Scott	(CADE-28) An Automated Approach to the Collatz Conjecture (WST 2021) Mixed Base Rewriting for the Collatz Conjecture
Abraham, Erika	(ARCADE 2021) Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Alrabbaa, Christian	(CADE-28) Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
B
Baader, Franz	(CADE-28) Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes (CADE-28) Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (CADE-28) Unification, Combination, Description Logics, and All That
Baelde, David	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
Barbosa, Haniel	(PxTP-7) Alethe: Towards a Generic SMT Proof Format (Extended Abstract)
Barnett, Lee	(CADE-28) Non-Clausal Redundancy Properties
Barrett, Clark	(CADE-28) Politeness and Stable Infiniteness: Stronger Together
Bartocci, Ezio	(CADE-28) A Normative Supervisor for Reinforcement Learning Agents (System Description)
Baudon, Thaïs	(WST 2021) Parallel Complexity of Term Rewriting Systems
Baumgartner, Peter	(CADE-28) The Fusemate Logic Programming System (System Description)
Ben-Amram, Amir	(WST 2021) Loops for which Multiphase-Linear Ranking Functions are Sufficient (WST 2021) Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs
Bentkamp, Alexander	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification (CADE-28) Making Higher-Order Superposition Work (CADE-28) Superposition for Full Higher-Order Logic
Benzmüller, Christoph	(CADE-28) Law, Morality, Religion, and ATP
Bibel, Wolfgang	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Biere, Armin	(CADE-28) Non-Clausal Redundancy Properties
Bjørner, Nikolaj	(CADE-28) Newbie's Meeting Place
Blackburn, Patrick	(ThEdu'21) Teaching Intuitionistic Propositional Logic Using Isabelle
Blanchette, Jasmin	(CADE-28) A Unifying Splitting Framework (CADE-28) Making Higher-Order Superposition Work (CADE-28) Superposition for Full Higher-Order Logic
Blot, Valentin	(PxTP-7) General Automation in Coq through Modular Transformations
Bonancina, Maria Paola	(PxTP-7) Proof Generation in CDSAT (CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Borgwardt, Stefan	(CADE-28) Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
Boyland, John	(ThEdu'21) Evolution of SASyLF 2008-2021
Brauße, Franz	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Bryant, Randal	(CADE-28) Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
Bártek, Filip	(CADE-28) Neural Precedence Recommender
C
Cao, Qinxiang	(LFMTP 2021) Countability of Inductive Types Formalized in the Object-Logic Level
Chaudhuri, Kaustuv	(CADE-28) Subformula Linking for Intuitionistic Logic and Type Theory
Ciabattoni, Agata	(CADE-28) A Normative Supervisor for Reinforcement Learning Agents (System Description)
Cimatti, Alessandro	(CADE-28) Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
Cohen, Liron	(CADE-28) Non-well-founded Deduction for Induction and Coinduction
Cruanes, Simon	(CADE-28) Making Higher-Order Superposition Work
Cuconato, Bruno	(LFMTP 2021) A logical framework with a graph meta-language
D
Davenport, James H.	(ARCADE 2021) Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
De Lon, Adrian	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
de Moura, Leonardo	(CADE-28) The Lean 4 Theorem Prover and Programming Language (System Description)
Delaune, Stephanie	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
Dershowitz, Nachum	(WST 2021) deVrijer’s Measure for SN of λ→ in Scheme
Desharnais, Martin	(CADE-28) Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Dixon, Clare	(CADE-28) Efficient Local Reductions to Basic Modal Logic
Do Vale, Deivid	(WST 2021) Formalizing Higher-Order Termination in Coq
Doménech, Jesús J.	(WST 2021) Loops for which Multiphase-Linear Ranking Functions are Sufficient
Donato, Pablo	(ThEdu'21) A Drag-and-Drop Proof Tactic
Dowek, Gilles	(ThEdu'21) How can we make Formal Proof Teachable? (LFMTP 2021) Interacting safely with an unsafe environment
Draheim, Dirk	(CADE-28) Confidences for Commonsense Reasoning
Dubois de Prisque, Louise	(PxTP-7) General Automation in Coq through Modular Transformations
E
Ebner, Gabriel	(CADE-28) A Unifying Splitting Framework (CADE-28) How can Anyone Trust a Theorem Prover?
Echenim, Mnacho	(CADE-28) Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Eisenhofer, Clemens	(ThEdu'21) Automated Instantiation of Control Flow Tracing Exercises
El-Beheiry, Laila	(LFMTP 2021) SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
Emrich, Frank	(WST 2021) Modular Termination Analysis of C Programs
England, Matthew	(ARCADE 2021) Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Errington, Jacob	(CADE-28) Harpoon: Mechanizing Metatheory Interactively (System Description)
F
Fiorentini, Camillo	(CADE-28) Efficient SAT-based proof search in Intuitionistic Propositional Logic
Fleury, Mathias	(PxTP-7) Alethe: Towards a Generic SMT Proof Format (Extended Abstract) (CADE-28) Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Fontaine, Pascal	(PxTP-7) Alethe: Towards a Generic SMT Proof Format (Extended Abstract) (CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Frohn, Florian	(WST 2021) Polynomial Loops: Termination and Beyond
From, Asta Halkjær	(ThEdu'21) Teaching Intuitionistic Propositional Logic Using Isabelle
Fuenmayor, David	(CADE-28) Law, Morality, Religion, and ATP
Fuhs, Carsten	(WST 2021) Between Derivational and Runtime Complexity (WST 2021) Parallel Complexity of Term Rewriting Systems
G
Garchery, Quentin	(PxTP-7) A Framework for Proof-Carrying Logical Transformations
Genaim, Samir	(WST 2021) Loops for which Multiphase-Linear Ranking Functions are Sufficient
Giesl, Jürgen	(CADE-28) 2021 Herbrand Award (WST 2021) Modular Termination Analysis of C Programs (WST 2021) Polynomial Loops: Termination and Beyond (WST 2021) Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Gocht, Stephan	(PxTP-7) Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
Golińska-Pilarek, Joanna	(CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity
Gonnord, Laure	(WST 2021) Parallel Complexity of Term Rewriting Systems
Governatori, Guido	(CADE-28) A Normative Supervisor for Reinforcement Learning Agents (System Description) (CADE-28) Computational Law: Automated Reasoning in the Legal Domain
Griggio, Alberto	(CADE-28) Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
H
Haeusler, Edward Hermann	(LFMTP 2021) A logical framework with a graph meta-language
Haifani, Fajar	(CADE-28) Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
Hark, Marcel	(WST 2021) Polynomial Loops: Termination and Beyond (WST 2021) Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Heisinger, Max	(PDAR-21) The Networked Uncertainty Principle, or How I Stopped Worrying and Love Local Tracing
Hensel, Jera	(WST 2021) Modular Termination Analysis of C Programs
Heule, Marijn	(CADE-28) An Automated Approach to the Collatz Conjecture (CADE-28) Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver (CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem (WST 2021) Mixed Base Rewriting for the Collatz Conjecture
Hozzová, Petra	(CADE-28) Integer Induction in Saturation
Hustadt, Ullrich	(CADE-28) Efficient Local Reductions to Basic Modal Logic
Huuskonen, Taneli	(CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity
I
Iosif, Radu	(CADE-28) Unifying Decidable Entailments in Separation Logic with Inductive Definitions
J
Jacomme, Charlie	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
Jang, Junyoung	(CADE-28) Harpoon: Mechanizing Metatheory Interactively (System Description)
Järv, Priit	(CADE-28) Confidences for Commonsense Reasoning
K
Karkour, Ammar	(LFMTP 2021) SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
Keller, Chantal	(PxTP-7) General Automation in Coq through Modular Transformations
Kim, Dohan	(CADE-28) Equational Theorem Proving Modulo
Koepke, Peter	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Koopmann, Patrick	(CADE-28) Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes (CADE-28) Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
Korovin, Konstantin	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Korovina, Margarita	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Koutny, Reinhard	(ThEdu'21) Make Isabelle Accessible!
Koutsos, Adrien	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
Kovtunova, Alisa	(CADE-28) Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
Kovács, Laura	(CADE-28) Integer Induction in Saturation (CADE-28) Newbie's Meeting Place (LFMTP 2021) Automating Induction by Reflection
Kovács, Zoltán	(ThEdu'21) Automated Discovery of Geometrical Theorems in GeoGebra (ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
Kremer, Gereon	(ARCADE 2021) Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Kriegel, Francesco	(CADE-28) Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
Krueger, Ryan	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Kumar, Ankit	(ThEdu'21) Automated Grading of Automata with ACL2s
L
Laarman, Alfons	(PDAR-21) Parallel Probabilistic Inference
Li, Liming	(CADE-28) Verified interactive computation of definite integrals
Lorenzen, Anton	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Lucas, Salvador	(WST 2021) Did Turing Care of the Halting Problem?
Lynch, Christopher	(CADE-28) Equational Theorem Proving Modulo
M
Magaud, Nicolas	(PxTP-7) Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract)
Manolios, Panagiotis	(ThEdu'21) Automated Grading of Automata with ACL2s
Maric, Filip	(ThEdu'21) Towards Next Step Guidance in Triangle Construction Problems
Marinković, Vesna	(ThEdu'21) Towards Next Step Guidance in Triangle Construction Problems
Marti, Adrian	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Martins, Ruben	(PxTP-7) Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
Meyer, Fabian	(WST 2021) Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Michael Han, Jesse	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Middeldorp, Aart	(WST 2021) Polynomial Termination over N is Undecidable
Miesenberger, Klaus	(ThEdu'21) Make Isabelle Accessible!
Mitterwallner, Fabian	(WST 2021) Polynomial Termination over N is Undecidable
Moreau, Solène	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
Müller, Norbert Th.	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
N
Nadathur, Gopalan	(LFMTP 2021) Adelfa: A System for Reasoning about LF Specifications
Nalon, Cláudia	(CADE-28) Efficient Local Reductions to Basic Modal Logic (CADE-28) Step into the Darkside - Non-classical Logics
Neufeld, Emery	(CADE-28) A Normative Supervisor for Reinforcement Learning Agents (System Description)
Neuper, Walther	(ThEdu'21) Make Isabelle Accessible!
Nigam, Vivek	(CADE-28) Proof Search and Certificates for Evidential Transactions
Nipkow, Tobias	(CADE-28) Isabelle's Metalogic: Formalization and Proof Checker
Nipkow, Tobias	(CADE-28) Isabelle: Growing and Applying a Proof Assistant
Nordstrom, Jakob	(PxTP-7) Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
Nummelin, Visa	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification (CADE-28) Making Higher-Order Superposition Work
Nuradiansyah, Adrian	(CADE-28) Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
O
Osama, Muhammad	(PDAR-21) GPU SAT Solving
Ozdemir, Alex	(PDAR-21) Constraint Solving in the Serverless Cloud
P
Papacchini, Fabio	(CADE-28) Efficient Local Reductions to Basic Modal Logic
Payet, Etienne	(WST 2021) Observing Loopingness
Pease, Adam	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes
Peltier, Nicolas	(CADE-28) Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Perdue, Crispin	(ThEdu'21) Prooftoys: a Proof Assistant for Beginners
Pientka, Brigitte	(CADE-28) Harpoon: Mechanizing Metatheory Interactively (System Description)
Piskac, Ruzica	(CADE-28) Newbie's Meeting Place
Plaisted, David	(ARCADE 2021) Management of the TPTP Problem Set (ARCADE 2021) Relevance and Abstraction (ARCADE 2021) Search Spaces for Theorem Proving Strategies
Platzer, André	(CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Q
Quaresma, Pedro	(ThEdu'21) Four Geometry Problems to Introduce Automated Deduction in Secondary Schools
R
Rabe, Florian	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Rabe, Markus N.	(CADE-28) Towards the Automatic Mathematician
Rahmouni, Samar	(CADE-28) Proof Search and Certificates for Evidential Transactions
Rawson, Michael	(PDAR-21) Parallel Tricks for Speedy Learned Guidance (ARCADE 2021) On Evaluating Theorem Provers
Redondi, Gianluca	(CADE-28) Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
Reger, Giles	(PxTP-7) Reasoning in Many Logics with Vampire: Everything's CNF in the End (PDAR-21) Hacking Shared Memory Parallelism in Vampire (ARCADE 2021) On Evaluating Theorem Provers
Reis, Carlos	(ThEdu'21) Four Geometry Problems to Introduce Automated Deduction in Secondary Schools
Reis, Giselle	(CADE-28) Proof Search and Certificates for Evidential Transactions (LFMTP 2021) SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts (LFMTP 2021) Facilitating Meta-Theory Reasoning
Reynolds, Andrew	(CADE-28) Politeness and Stable Infiniteness: Stronger Together
Riener, Martin	(ThEdu'21) Automated Instantiation of Control Flow Tracing Exercises
Ringeissen, Christophe	(CADE-28) Politeness and Stable Infiniteness: Stronger Together
Roux, Navid	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Roßkopf, Simon	(CADE-28) Isabelle's Metalogic: Formalization and Proof Checker
Ruess, Harald	(CADE-28) Proof Search and Certificates for Evidential Transactions
S
Sagiv, Mooly	(CADE-28) Formal Reasoning about Decentralized Financial Applications
Santos, Jefferson de Barros	(LFMTP 2021) A logical framework with a graph meta-language
Schlichtkrull, Anders	(CADE-28) How can Anyone Trust a Theorem Prover?
Schoisswohl, Johannes	(LFMTP 2021) Automating Induction by Reflection
Schulz, Stephan	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes (CADE-28) 17 Ways to make an ATP System Fast
Schurr, Hans-Jörg	(PxTP-7) Alethe: Towards a Generic SMT Proof Format (Extended Abstract) (CADE-28) Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Schütz, Marcel	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Selsam, Daniel	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Sheng, Ying	(CADE-28) Politeness and Stable Infiniteness: Stronger Together
Smallbone, Nicholas	(CADE-28) Twee: an equational theorem prover (System Description)
Southern, Mary	(LFMTP 2021) Adelfa: A System for Reasoning about LF Specifications
Sozeau, Matthieu	(LFMTP 2021) The MetaCoq Project
Steen, Alexander	(CADE-28) Step into the Darkside - Non-classical Logics
Strub, Pierre-Yves	(ThEdu'21) A Drag-and-Drop Proof Tactic
Stöger, Bernhard	(ThEdu'21) Make Isabelle Accessible!
Suda, Martin	(CADE-28) Neural Precedence Recommender (CADE-28) Improving ENIGMA-Style Clause Selection While Learning From History
Sutcliffe, Geoff	(CADE-28) The CADE-28 ATP System Competition (CASC-28) Results (CADE-28) Reception Opening (ARCADE 2021) The Expansion, Modernisation, and Future of the TPTP World (ARCADE 2021) Management of the TPTP Problem Set
Szegedy, Christian	(CADE-28) Towards the Automatic Mathematician
T
Tammet, Tanel	(CADE-28) Confidences for Commonsense Reasoning
Tinelli, Cesare	(CADE-28) Politeness and Stable Infiniteness: Stronger Together
Tourret, Sophie	(CADE-28) Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance (CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification (CADE-28) A Unifying Splitting Framework (CADE-28) Making Higher-Order Superposition Work (CADE-28) Superposition for Full Higher-Order Logic
U
Ullrich, Sebastian	(CADE-28) The Lean 4 Theorem Prover and Programming Language (System Description)
V
Vajda, Robert	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
van der Weide, Niels	(WST 2021) Formalizing Higher-Order Termination in Coq
van Dijk, Tom	(PDAR-21) Demonstrating Work-stealing with Lace and its Application in Sylvan
Vial, Pierre	(PxTP-7) General Automation in Coq through Modular Transformations
Villadsen, Jørgen	(ThEdu'21) Teaching Intuitionistic Propositional Logic Using Isabelle
Voronkov, Andrei	(CADE-28) Integer Induction in Saturation (CADE-28) 2020 Herbrand Award
Vukmirović, Petar	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification (CADE-28) Making Higher-Order Superposition Work (CADE-28) Superposition for Full Higher-Order Logic (CADE-28) 17 Ways to make an ATP System Fast
W
Walter, Andrew	(ThEdu'21) Automated Grading of Automata with ACL2s
Wang, Anduo	(LFMTP 2021) Towards a Semantic Framework for Policy Exchange in the Internet
Weidenbach, Christoph	(CADE-28) Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance (CADE-28) Break
Wenzel, Makarius	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Werner, Benjamin	(ThEdu'21) A Drag-and-Drop Proof Tactic
Wernhard, Christoph	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Wu, Xiwei	(LFMTP 2021) Countability of Inductive Types Formalized in the Object-Logic Level
X
Xu, Runqing	(CADE-28) Verified interactive computation of definite integrals
Y
Yamada, Akihisa	(CADE-28) Multi-Dimensional Interpretation Methods for Termination of Term Rewriting (CADE-28) Termination and Complexity Competition Results
Yolcu, Emre	(CADE-28) An Automated Approach to the Collatz Conjecture (WST 2021) Mixed Base Rewriting for the Collatz Conjecture
Yu, Jonathan H.	(ThEdu'21) Automated Discovery of Geometrical Theorems in GeoGebra
Z
Zawidzki, Michał	(CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity
Zhan, Bohua	(CADE-28) Verified interactive computation of definite integrals
Zohar, Yoni	(CADE-28) Politeness and Stable Infiniteness: Stronger Together

Disclaimer | Powered by EasyChair Smart Program