| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Mingshuai Chen, Jian Wang 0042, Jie An 0001, Bohua Zhan, Deepak Kapur, Naijun Zhan |
NIL: Learning Nonlinear Interpolants.  |
CADE  |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
Model Completeness, Covers and Superposition. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach |
SPASS-SATT - A CDCL(LA) Solver. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Rose Bohrer, Manuel Fernández 0005, André Platzer |
dLι: Definite Descriptions in Differential Dynamic Logic. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Fiori, Christoph Weidenbach |
SCL Clause Learning from Simple Models. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Aina Niemetz, Mathias Preiner, Andrew Reynolds 0001, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
Towards Bit-Width-Independent Proofs in SMT Solvers. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Ahmed Bhayat, Giles Reger |
Restricted Combinatory Unification. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann |
Superposition with Lambdas. |
CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar |
Satisfiability Modulo Theories and Assignments. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Baoluo Meng, Andrew Reynolds 0001, Cesare Tinelli, Clark W. Barrett |
Relational Constraint Solving in SMT. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Kiesl, Martin Suda 0001 |
A Unifying Principle for Clause Elimination in First-Order Logic. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
Satisfiability Modulo Transcendental Functions via Incremental Linearization. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Markus Bender, Viorica Sofronie-Stokkermans |
Decision Procedures for Theories of Sets with Measures. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Cruanes |
Satisfiability Modulo Bounded Checking. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Nicolas Peltier |
The Binomial Pricing Model in Finance: A Formalization in Isabelle. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhaowei Xu, Taolue Chen, Zhilin Wu |
Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine |
Scalable Fine-Grained Proofs for Formula Processing. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Horbach, Marco Voigt, Christoph Weidenbach |
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Schulz 0001, Geoff Sutcliffe, Josef Urban, Adam Pease |
Detecting Inconsistencies in Large First-Order Knowledge Bases. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | José Fragoso Santos, Philippa Gardner, Petar Maksimovic, Daiva Naudziuniene |
Towards Logic-Based Verification of JavaScript Programs. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Ullrich Hustadt, Ana Ozaki, Clare Dixon |
Theorem Proving for Metric Temporal Logic over the Naturals. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | James Brotherston, Nikos Gorogiannis, Max I. Kanovich |
Biabduction (and Related Problems) in Array Separation Logic. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Yutaka Nagashima, Ramana Kumar |
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Lonsing, Uwe Egly |
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo de Moura 0001 (eds.) |
Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Petros Papapanagiotou, Jacques D. Fleuriot |
WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Marijn J. H. Heule, Benjamin Kiesl, Armin Biere |
Short Proofs Without New Variables. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Maximiliano Cristiá, Gianfranco Rossi |
A Decision Procedure for Restricted Intensional Sets. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Gadi Tellez, James Brotherston |
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp |
Efficient Certified RAT Verification. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen |
Notions of Knowledge in Combinations of Theories Sharing Constructors. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Teucke, Christoph Weidenbach |
Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Julian Nagele, Bertram Felgenhauer, Aart Middeldorp |
CSI: New Evidence - A Progress Report. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | June Andronick |
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernhard Gleiss, Laura Kovács, Martin Suda 0001 |
Splitting Proofs for Interpolation. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo |
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Sternagel, Thomas Sternagel |
Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Grant Olney Passmore, Denis Ignatovich |
Formal Verification of Financial Algorithms. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Blanco, Zakaria Chihani, Dale Miller 0001 |
Translating Between Implicit and Explicit Versions of Proof. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Färber 0002, Cezary Kaliszyk, Josef Urban |
Monte Carlo Tableau Proof Search. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich |
Efficient Verified (UN)SAT Certificate Checking. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002 |
Certifying Safety and Termination Proofs for Integer Transition Systems. |
CADE |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Amélie David 0001 |
Deciding ATL*Satisfiability by Tableaux. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Salman Saghafi, Ryan Danas, Daniel J. Dougherty |
Exploring Theories with a Model-Finding Assistant. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Kailiang Ji |
CTL Model Checking in Deduction Modulo. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
Expressing Symmetry Breaking in DRAT Proofs. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Takahito Aoto 0001, Nao Hirokawa, Julian Nagele, Naoki Nishida 0001, Harald Zankl |
Confluence Competition 2015. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhe Hou, Rajeev Goré, Alwen Tiu |
Automated Theorem Proving for Assertions in Separation Logic with All Connectives. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer |
The Lean Theorem Prover (System Description). |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai |
Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Bromberger, Thomas Sturm 0001, Christoph Weidenbach |
Linear Integer Arithmetic Revisited. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Ulrich Furbach, Björn Pelzer, Claudia Schon |
Automated Reasoning in the Wild. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner 0001 |
SMTtoTPTP - A Converter for Theorem Proving Formats. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka, Andrew Cave |
Inductive Beluga: Programming Proofs. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Crystal Chang Din, Richard Bubel, Reiner Hähnle |
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Giles Reger, Dmitry Tishkovsky, Andrei Voronkov |
Cooperating Proof Attempts. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Philippe Balbiani, Joseph Boudou |
Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Plaisted |
History and Prospects for First-Order Automated Deduction. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Ursula Martin |
Stumbling Around in the Dark: Lessons from Everyday Mathematics. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer |
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Haruhiko Sato, Sarah Winkler |
Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Backeman, Philipp Rümmer |
Theorem Proving with Bounded Rigid E-Unification. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Gorzny, Bruno Woltzenlogel Paleo |
Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Giles Reger, Martin Suda 0001, Andrei Voronkov |
Playing with AVATAR. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesse Alama, Paul E. Oppenheimer, Edward N. Zalta |
Automating Leibniz's Theory of Concepts. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa |
Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Kiraku Shintani, Nao Hirokawa |
CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Vijay D'Silva, Caterina Urban |
Abstract Interpretation as Automated Deduction. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Stephan Schulz 0001, Josef Urban, Jirí Vyskocil |
System Description: E.T. 0.1. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty, Aart Middeldorp (eds.) |
Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Gransden, Neil Walkinshaw, Rajeev Raman |
SEPIA: Search for Proofs Using Inferred Automata. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Filip Maric, Predrag Janicic, Marko Malikovic |
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Reynolds 0001, Jasmin Christian Blanchette |
A Decision Procedure for (Co)datatypes in SMT Solvers. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Grant Olney Passmore |
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki 0001 |
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleks Kissinger, Vladimir Zamdzhiev |
Quantomatic: A Proof Assistant for Diagrammatic Reasoning. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann |
Termination Competition (termCOMP 2015). |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner 0001, Joshua Bax, Uwe Waldmann |
Beagle - A Hierarchic Superposition Theorem Prover. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
Quantifier-Free Equational Logic and Prime Implicate Generation. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
A Formalisation of Finite Automata Using Hereditarily Finite Sets. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | José Iborra, Naoki Nishida 0001, Germán Vidal, Akihisa Yamada 0002 |
Reducing Relative Termination to Dependency Pair Problems. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen |
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | André Platzer |
A Uniform Substitution Calculus for Differential Dynamic Logic. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Ashish Tiwari 0001, Adrià Gascón, Bruno Dutertre |
Program Synthesis Using Dual Interpretation. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Tomer Libal |
Regular Patterns in Second-Order Unification. |
CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Josef Urban |
PRocH: Proof Reconstruction for HOL Light. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Marta Cialdea Mayer |
A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Graeme Gange, Harald Søndergaard, Peter J. Stuckey, Peter Schachte |
Solving Difference Constraints over Modular Arithmetic. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Richard Williams, Boris Konev |
Propositional Temporal Proving with Reductions to a SAT Problem. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Krystof Hoder, Andrei Voronkov |
The 481 Ways to Split a Clause and Deal with Propositional Variables. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernhard Beckert, Daniel Bruns |
Dynamic Logic with Trace Semantics. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Viorica Sofronie-Stokkermans |
Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Zakaria Chihani, Dale Miller 0001, Fabien Renaud |
Foundational Proof Certificates in First-Order Logic. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Markus Bender, Björn Pelzer, Claudia Schon |
System Description: E-KRHyper 1.4 - Extensions for Unique Names and Description Logic. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Franz Baader, Stefan Borgwardt, Marcel Lippmann |
Temporalizing Ontology-Based Data Access. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark Kaminski, Tobias Tebbi |
InKreSAT: Modal Reasoning via Incremental Reduction to SAT. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Radu Iosif, Adam Rogalewicz, Jirí Simácek |
The Tree Width of Separation Logic with Recursive Definitions. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Serdar Erbatur, Santiago Escobar 0001, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows 0001, José Meseguer 0001, Paliath Narendran, Sonia Santiago, Ralf Sasse |
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Reynolds 0001, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett |
Quantifier Instantiation Techniques for Finite Model Finding in SMT. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license