![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
28th CADE 2021: Virtual Event
- André Platzer
, Geoff Sutcliffe
:
Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. Lecture Notes in Computer Science 12699, Springer 2021, ISBN 978-3-030-79875-8
Invited Talks
- Liron Cohen
:
Non-well-founded Deduction for Induction and Coinduction. 3-24 - Markus N. Rabe
, Christian Szegedy
:
Towards the Automatic Mathematician. 25-37
Logical Foundations
- Joanna Golinska-Pilarek
, Taneli Huuskonen
, Michal Zawidzki
:
Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity. 41-57 - Christoph Wernhard
, Wolfgang Bibel
:
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures. 58-75 - Fabio Papacchini
, Cláudia Nalon
, Ullrich Hustadt
, Clare Dixon
:
Efficient Local Reductions to Basic Modal Logic. 76-92 - Tobias Nipkow
, Simon Roßkopf
:
Isabelle's Metalogic: Formalization and Proof Checker. 93-110
Theory and Principles
- Franz Brauße
, Konstantin Korovin
, Margarita V. Korovina
, Norbert Th. Müller
:
The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. 113-130 - Alessandro Cimatti
, Alberto Griggio
, Gianluca Redondi
:
Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. 131-147 - Ying Sheng
, Yoni Zohar
, Christophe Ringeissen
, Andrew Reynolds
, Clark W. Barrett
, Cesare Tinelli
:
Politeness and Stable Infiniteness: Stronger Together. 148-165 - Dohan Kim
, Christopher Lynch
:
Equational Theorem Proving Modulo. 166-182 - Mnacho Echenim
, Radu Iosif
, Nicolas Peltier
:
Unifying Decidable Entailments in Separation Logic with Inductive Definitions. 183-199 - Kaustuv Chaudhuri
:
Subformula Linking for Intuitionistic Logic with Application to Type Theory. 200-216 - Camillo Fiorentini
:
Efficient SAT-based Proof Search in Intuitionistic Propositional Logic. 217-233 - Vivek Nigam
, Giselle Reis
, Samar Rahmouni
, Harald Ruess
:
Proof Search and Certificates for Evidential Transactions. 234-251 - Lee A. Barnett
, Armin Biere
:
Non-clausal Redundancy Properties. 252-272 - Akihisa Yamada
:
Multi-Dimensional Interpretations for Termination of Term Rewriting. 273-290 - Christian Alrabbaa
, Franz Baader
, Stefan Borgwardt
, Patrick Koopmann
, Alisa Kovtunova
:
Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures. 291-308 - Franz Baader
, Patrick Koopmann
, Francesco Kriegel
, Adrian Nuradiansyah
:
Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes. 309-326 - Fajar Haifani
, Sophie Tourret
, Christoph Weidenbach
:
Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. 327-343 - Gabriel Ebner
, Jasmin Blanchette
, Sophie Tourret
:
A Unifying Splitting Framework. 344-360 - Petra Hozzová
, Laura Kovács
, Andrei Voronkov:
Integer Induction in Saturation. 361-377 - Visa Nummelin
, Alexander Bentkamp
, Sophie Tourret
, Petar Vukmirovic
:
Superposition with First-class Booleans and Inprocessing Clausification. 378-395 - Alexander Bentkamp
, Jasmin Blanchette
, Sophie Tourret
, Petar Vukmirovic
:
Superposition for Full Higher-order Logic. 396-412
Implementation and Application
- Petar Vukmirovic
, Alexander Bentkamp
, Jasmin Blanchette
, Simon Cruanes
, Visa Nummelin
, Sophie Tourret
:
Making Higher-Order Superposition Work. 415-432 - Randal E. Bryant
, Marijn J. H. Heule
:
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. 433-449 - Hans-Jörg Schurr
, Mathias Fleury
, Martin Desharnais
:
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. 450-467 - Emre Yolcu
, Scott Aaronson, Marijn J. H. Heule
:
An Automated Approach to the Collatz Conjecture. 468-484 - Runqing Xu
, Liming Li
, Bohua Zhan
:
Verified Interactive Computation of Definite Integrals. 485-503
ATP and AI
- Tanel Tammet
, Dirk Draheim
, Priit Järv
:
Confidences for Commonsense Reasoning. 507-524 - Filip Bártek
, Martin Suda
:
Neural Precedence Recommender. 525-542 - Martin Suda
:
Improving ENIGMA-style Clause Selection while Learning From History. 543-561
System Descriptions
- Emery A. Neufeld
, Ezio Bartocci
, Agata Ciabattoni
, Guido Governatori
:
A Normative Supervisor for Reinforcement Learning Agents. 565-576 - Ryan Krueger
, Jesse Michael Han, Daniel Selsam:
Automatically Building Diagrams for Olympiad Geometry Problems. 577-588 - Peter Baumgartner
:
The Fusemate Logic Programming System. 589-601 - Nicholas Smallbone
:
Twee: An Equational Theorem Prover. 602-613 - Adrian De Lon
, Peter Koepke
, Anton Lorenzen
, Adrian Marti
, Marcel Schütz
, Makarius Wenzel
:
The Isabelle/Naproche Natural Language Proof Assistant. 614-624 - Leonardo de Moura
, Sebastian Ullrich
:
The Lean 4 Theorem Prover and Programming Language. 625-635 - Jacob Errington
, Junyoung Jang
, Brigitte Pientka
:
Harpoon: Mechanizing Metatheory Interactively - (System Description). 636-648
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.