Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Simon Colton, Sophie Huczynska |
The Homer System. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Harald Ganzinger, Jürgen Stuber |
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Renate A. Schmidt, Ullrich Hustadt |
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Nao Hirokawa, Aart Middeldorp |
Automating the Dependency Pair Method. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Aaron Stump |
Subset Types and Partial Functions. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Sava Krstic, Sylvain Conchon |
Canonization for Disjoint Unions of Theories. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Sumit Gulwani, George C. Necula |
A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Guoqiang Pan, Moshe Y. Vardi |
Optimizing a BDD-Based Modal Solver. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge |
Certifying Solutions to Permutation Group Problems. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Edmund M. Clarke |
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Joe Hurd |
An LCF-Style Interface between HOL and First-Order Logic. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi |
The Complexity of the Graded µ-Calculus. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Larchey-Wendling |
Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Zimmer, Michael Kohlhase |
System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Jonathan Ford, Natarajan Shankar |
Formal Verification of a Combination Decision Procedure. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Mateja Jamnik, Manfred Kerber, Martin Pollet |
Learn Omega-matic: System Description. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Boy de la Tour |
A Note on Symmetry Heuristics in SEM. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Simon Colton |
The HR Program for Theorem Generation. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Martin Strecker |
Formal Verification of a Java Compiler in Isabelle. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Jörg H. Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke 0001, Helmut Horacek, Michael Kohlhase, Andreas Meier 0002, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, Jürgen Zimmer |
Proof Development with OMEGA. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Miquel Bofill, Albert Rubio |
Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobalt, Dalibor Topic |
S PASS Version 2.0. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Chad E. Brown |
Solving for Set Variables in Higher-Order Theorem Proving. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Michael W. Whalen, Johann Schumann, Bernd Fischer 0002 |
AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Marc Andreoli |
Focussing Proof-Net Construction as a Middleware Paradigm. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
Proof construction, Focussing, Middleware, Transactions, Proof search, Proof-nets |
1 | Cristina Borralleras, Salvador Lucas, Albert Rubio |
Recursive Path Orderings Can Be Context-Sensitive. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Didier Galmiche, Daniel Méry |
Connection-Based Proof Search in Propositional BI Logic. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Uwe Egly |
Embedding Lax Logic into Intuitionistic Logic. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Calogero G. Zarba |
Combining Multisets with Integers. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Aaron Stump, David L. Dill |
Faster Proof Checking in the Edinburgh Logical Framework. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt |
A New Clausal Class Decidable by Hyperresolution. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Carlos Areces, Juan Heguiabehere |
HyLoRes 1.0: Direct Resolution for Hybrid Logics. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Gramlich, Reinhard Pichler |
Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea |
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Harald Ganzinger |
Shostak Light. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Andrew Bernard, Peter Lee 0001 |
Temporal Logic for Proof-Carrying Code. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
temporal logic, Proof-carrying code |
1 | Christopher Lynch, Barbara Morawska 0001 |
Basic Syntactic Mutation. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Eugene Goldberg |
Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Jesper B. Møller |
DDDLIB: A Library for Solving Quantified Difference Inequalities. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Andrei Voronkov (eds.) |
Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Lawrence C. Paulson |
The Reflection Theorem: A Study in Meta-theoretic Reasoning. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Stephan Schulz 0001, Geoff Sutcliffe |
System Description: GrAnDe 1.0. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Audemard, Belaid Benhamou |
Reasoning by Symmetry and Function Ordering in Finite Model Generation. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Baaz |
Proof Analysis by Resolution. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi |
BDD-Based Decision Procedures for K. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Hillenbrand, Bernd Löchner |
The Next W ALDMEISTER Loop. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Lintao Zhang, Sharad Malik |
The Quest for Efficient Boolean Satisfiability Solvers. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Ian Horrocks 0001 |
Reasoning with Expressive Description Logics: Theory and Practice. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Robert R. Schneck, George C. Necula |
A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Ahrendt |
Deductive Search for Errors in Free Data Type Specifications Using Model Generation. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Carsten Schürmann |
Workshop: Automation of Proofs by Mathematical Induction. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
High-Level Verification Using Theorem Proving and Formalized Mathematics. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Marc Bezem, Dimitri Hendriks, Hans de Nivelle |
Automated Proof Construction in Type Theory Using Resolution. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe |
System Description: SystemOn TPTP. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Carsten Schürmann |
Tutorial: Meta-logical Frameworks. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Stephen G. Pulman |
Tutorial: Automated Deduction and Natural Language Understanding. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Audemard, Belaid Benhamou, Laurent Henocque |
Two Techniques to Improve Finite Model Search. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Renate A. Schmidt, Ullrich Hustadt |
A Resolution Decision Procedure for Fluted Logic. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Erica Melis |
Workshop: Automated Deduction in Education. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Simon Colton, Volker Sorge, Ursula Martin |
Workshop: The Role of Automated Deduction in Mathematics. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Graham Collins, Louise A. Dennis |
System Description: Embedding Verification into Microsoft Excel. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Peter B. Andrews, Chad E. Brown |
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Doron Bustan, Orna Grumberg |
Simulation Based Minimization. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | George C. Necula, Peter Lee 0001 |
Proof Generation in the Touchstone Theorem Prover. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Mike Jackson 0003, Helen Lowe |
System Description: Interactive Proof Critics in XBarnacle. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Ian Horrocks 0001, Ulrike Sattler, Stephan Tobies |
Reasoning with Individuals for the Description Logic SHIQ. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Bruce Spencer, Joseph Douglas Horton |
Support Ordered Resolution. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Meier 0002 |
System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Carl-Johan H. Seger |
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001 |
FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Neophytos G. Michael, Andrew W. Appel |
Machine Instruction Syntax and Semantics in Higher Order Logic. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Konrad Slind |
Wellfounded Schematic Definitions. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | E. Allen Emerson, Vineet Kahlon |
Reducing Model Checking of the Many to the Few. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Clark W. Barrett, David L. Dill, Aaron Stump |
A Framework for Cooperating Decision Procedures. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Carsten Sinz |
System Description: ARA - An Automatic Theorem Prover for Relation Algebras. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Genet, Francis Klay |
Rewriting for Cryptographic Protocol Verification. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Peter B. Andrews, Matthew Bishop, Chad E. Brown |
System Description: TPS: A Theorem Proving System for Type Theory. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | William M. Farmer |
An Infrastructure for Intertheory Reasoning. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Florian Kammüller |
Modular Reasoning in Isabelle. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Guillaume Gillard |
A Formalization of a Concurrent Object Calculus up to alpha-Conversion. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo |
The Nuprl Open Logical Environment. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Johan G. F. Belinfante |
Gödel's Algorithm for Class Formation. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Ashish Tiwari 0001, Leo Bachmair, Harald Rueß |
Rigid E-Unification Revisited. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Anatoli Degtyarev, Andrei Voronkov |
Stratified Resolution. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Leo Bachmair, Ashish Tiwari 0001 |
Abstract Congruence Closure and Specializations. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | David A. McAllester (eds.) |
Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Enrico Giunchiglia, Armando Tacchella |
System Description: *SAT: A Platform for the Development of Modal Decision Procedures. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Giesl, Aart Middeldorp |
Eliminating Dummy Elimination. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Henry A. Kautz |
Scalable Knowledge Representation and Reasoning Systems. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Franke 0001, Michael Kohlhase |
System Description: MBASE, an Open Mathematical Knowledge Base. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Deepak Kapur, Mahadevan Subramaniam |
Extending Decision Procedures with Induction Schemes. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Cristina Borralleras, Maria Ferreira, Albert Rubio |
Complete Monotonic Semantic Path Orderings. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Ryuzo Hasegawa, Hiroshi Fujita 0002, Miyuki Koshimura |
Efficient Minimal Model Generation Using Branching Lemmas. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang 0001 |
Workshop: Model Computation - Principles, Algorithms, Applications. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Peter F. Patel-Schneider |
System Description: DLP. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Didier Galmiche |
Workshop: Type-Theoretic Languages: Proof-Search and Semantics. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Viorica Sofronie-Stokkermans |
On Unification for Bonded Distributive Lattices. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Marianne Brown, Geoff Sutcliffe |
System Description: PTTP+GLiDes: Semantically Guided PTTP. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
1 | William McCune, Olga Shumsky |
System Description: IVY. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|