| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Oliver Görlitz, Daniel Hausmann 0001, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schröder |
COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description).  |
CADE  |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Nikolaj S. Bjørner, Katalin Fazekas |
On Incremental Pre-processing for SMT. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonas Schöpf, Aart Middeldorp |
Confluence Criteria for Logically Constrained Rewrite Systems. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu |
Iscalc: An Interactive Symbolic Computation Framework (System Description). |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan-Christoph Kassing, Jürgen Giesl |
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jera Hensel, Jürgen Giesl |
Proving Termination of C Programs with Lists. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson 0001 |
Superposition with Delayed Unification. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Colin Rothgang, Florian Rabe 0001, Christoph Benzmüller |
Theorem Proving in Dependently-Typed Higher-Order Logic. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Gerald Whitters, Vivek Nigam, Carolyn L. Talcott |
Incremental Rewriting Modulo SMT. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Yu-Fang Chen 0001, Philipp Rümmer, Wei-Lun Tsai |
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Bruse, Martin Lange, Sören Möller |
Formal Reasoning About Influence in Natural Sciences Experiments. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier |
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Manfred Schmidt-Schauß, Daniele Nantes-Sobrinho |
Towards Fast Nominal Anti-unification of Letrec-Expressions. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrzej Indrzejczak, Yaroslav I. Petrukhin |
A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon |
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Tanel Tammet, Priit Järv, Martin Verrev, Dirk Draheim |
An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper). |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Frohn, Jürgen Giesl |
Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper). |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Blanchette, Qi Qiu, Sophie Tourret |
Verified Given Clause Procedures. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov |
Program Synthesis in Saturation. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka, Cesare Tinelli (eds.) |
Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Lukas Stevens |
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Tomás Fiedor, Lukás Holík, Martin Hruska, Adam Rogalewicz, Juraj Síc, Pavol Vargovcík |
Reasoning About Regular Properties: A Comparative Study. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler |
Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Bromberger, Chaahat Jain, Christoph Weidenbach |
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Bromberger, Martin Desharnais, Christoph Weidenbach |
An Isabelle/HOL Formalization of the SCL(FOL) Calculus. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett |
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Robin Coutelier, Laura Kovács, Michael Rawson 0001, Jakob Rath |
SAT-Based Subsumption Resolution. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Marvin Brieger, Stefan Mitsch, André Platzer |
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Katharina Kreuzer, Tobias Nipkow |
Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremias Berg, Bart Bogaerts 0001, Jakob Nordström, Andy Oertel, Dieter Vandesande |
Certified Core-Guided MaxSAT Solving. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Dennis Peuter, Viorica Sofronie-Stokkermans, Sebastian Thunert |
On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics Eℒ, Eℒ+. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp |
Left-Linear Completion with AC Axioms. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernard Boigelot, Pascal Fontaine, Baptiste Vergain |
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Mathias Fleury, Peter Lammich |
A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Tanel Tammet, Dirk Draheim, Priit Järv |
Confidences for Commonsense Reasoning. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais |
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Joanna Golinska-Pilarek, Taneli Huuskonen, Michal Zawidzki |
Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, Alisa Kovtunova |
Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Emre Yolcu, Scott Aaronson, Marijn J. H. Heule |
An Automated Approach to the Collatz Conjecture. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Ying Sheng 0007, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds 0001, Clark W. Barrett, Cesare Tinelli |
Politeness and Stable Infiniteness: Stronger Together. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Filip Bártek, Martin Suda 0001 |
Neural Precedence Recommender. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Vivek Nigam, Giselle Reis, Samar Rahmouni, Harald Ruess |
Proof Search and Certificates for Evidential Transactions. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacob Errington, Junyoung Jang 0001, Brigitte Pientka |
Harpoon: Mechanizing Metatheory Interactively - (System Description). |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Ryan Krueger, Jesse Michael Han, Daniel Selsam |
Automatically Building Diagrams for Olympiad Geometry Problems. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Markus N. Rabe, Christian Szegedy |
Towards the Automatic Mathematician. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller |
The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Camillo Fiorentini |
Efficient SAT-based Proof Search in Intuitionistic Propositional Logic. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon |
Efficient Local Reductions to Basic Modal Logic. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel |
The Isabelle/Naproche Natural Language Proof Assistant. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret |
Making Higher-Order Superposition Work. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Emery A. Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori |
A Normative Supervisor for Reinforcement Learning Agents. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic |
Superposition for Full Higher-order Logic. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Kaustuv Chaudhuri |
Subformula Linking for Intuitionistic Logic with Application to Type Theory. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Liron Cohen 0001 |
Non-well-founded Deduction for Induction and Coinduction. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Gianluca Redondi |
Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo de Moura 0001, Sebastian Ullrich 0002 |
The Lean 4 Theorem Prover and Programming Language. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Franz Baader, Patrick Koopmann, Francesco Kriegel, Adrian Nuradiansyah |
Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Radu Iosif, Nicolas Peltier |
Unifying Decidable Entailments in Separation Logic with Inductive Definitions. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Suda 0001 |
Improving ENIGMA-style Clause Selection while Learning From History. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Marijn J. H. Heule |
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | André Platzer, Geoff Sutcliffe (eds.) |
Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Runqing Xu, Liming Li, Bohua Zhan |
Verified Interactive Computation of Definite Integrals. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow, Simon Roßkopf |
Isabelle's Metalogic: Formalization and Proof Checker. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicholas Smallbone |
Twee: An Equational Theorem Prover. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Lee A. Barnett, Armin Biere |
Non-clausal Redundancy Properties. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Petra Hozzová, Laura Kovács, Andrei Voronkov |
Integer Induction in Saturation. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriel Ebner, Jasmin Blanchette, Sophie Tourret |
A Unifying Splitting Framework. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner 0001 |
The Fusemate Logic Programming System. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Fajar Haifani, Sophie Tourret, Christoph Weidenbach |
Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Wernhard, Wolfgang Bibel |
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Dohan Kim 0001, Christopher Lynch |
Equational Theorem Proving Modulo. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic |
Superposition with First-class Booleans and Inprocessing Clausification. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Akihisa Yamada 0002 |
Multi-Dimensional Interpretations for Termination of Term Rewriting. |
CADE |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | André Platzer |
Uniform Substitution at One Fell Swoop. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar |
Automata Terms in a Lazy WSkS Decision Procedure. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michaël Rusinowitch |
Unification Modulo Lists with Reverse Relation with Certain Word Equations. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Pascal Fontaine (eds.) |
Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Katherine Cordwell, André Platzer |
Towards Physical Hybrid Systems. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Christina Kohl, Aart Middeldorp |
Composing Proof Terms. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexsander Andrade de Melo, Mateus de Oliveira Oliveira |
On the Width of Regular Classes of Finite Structures. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Sternagel, Sarah Winkler |
Certified Equational Reasoning via Ordered Completion. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Rawson 0001, Giles Reger |
Old or Heavy? Decaying Gracefully with Age/Weight Shapes. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Yizheng Zhao, Renate A. Schmidt |
FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi |
Confluence by Critical Pair Analysis Revisited. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Schulz 0001, Simon Cruanes, Petar Vukmirovic |
Faster, Higher, Stronger: E 2.3. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Geoff Sutcliffe, Francis Jeffry Pelletier |
JGXYZ: An ATP System for Gap and Glut Logics. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Ulrich Furbach, Teresa Krämer, Claudia Schon |
Names Are Not Just Sound and Smoke: Word Embeddings for Axiom Selection. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Jürgen Giesl, Peter Giesl, Marcel Hark |
Computing Expected Runtimes for Constant Probability Programs. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Giles Reger, Andrei Voronkov |
Induction in Saturation-Based Proof Search. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Plaisted |
The Aspect Calculus. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Raúl Gutiérrez, Salvador Lucas |
Automatic Generation of Logical Models with AGES. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Valentin Cassano, Raul Fervari, Guillaume Hoffmann 0001, Carlos Areces, Pablo F. Castro |
A Tableaux Calculus for Default Intuitionistic Logic. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Haniel Barbosa, Andrew Reynolds 0001, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett |
Extending SMT Solvers to Higher-Order Logic. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrei Popescu 0001, Dmitriy Traytel |
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Dennis Peuter, Viorica Sofronie-Stokkermans |
On Invariant Synthesis for Parametric Systems. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Di Long Li, Alwen Tiu |
Combining ProVerif and Automated Theorem Provers for Security Protocol Verification. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Trentin, Roberto Sebastiani |
Optimization Modulo the Theory of Floating-Point Numbers. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Tanel Tammet |
GKC: A Reasoning System for Large Knowledge Bases. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban |
GRUNGE: A Grand Unified ATP Challenge. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Karel Chvalovský, Jan Jakubuv, Martin Suda 0001, Josef Urban |
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license