| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Philippe Chatalic, Laurent Simon |
ZRES: The Old Davis-Putman Procedure Meets ZBDD.  |
CADE  |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Jon Whittle 0001, Alan Bundy, Richard J. Boulton, Helen Lowe |
System Description: CyNTHIA. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury |
Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Predrag Janicic, Alan Bundy, Ian Green |
A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Raul H. C. Lopes |
Automatic Generation of Proof Search Strategies for Second-order Logic. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Franke 0001, Michael Kohlhase |
System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow |
Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract). |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Reinhard Pichler |
Solving Equational Problems Efficiently. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Carlos Areces, Hans de Nivelle, Maarten de Rijke |
Prefixed Resolution: A Resolution Method for Modal and Description Logics. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Viorica Sofronie-Stokkermans |
On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Schulz 0001 |
System Abstract: E 0.3. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Jason Hickey |
Fault-Tolerant Distributed Theorem Proving. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Erich Grädel |
Invited Talk: Decision procedures for guarded logics. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer |
System Description: inka 5.0 - A Logic Voyager. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Jian Zhang 0001 |
System Description: MCS: Model-based Conjecture Searching. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Weidenbach |
System Description: Spass Version 1.0.0. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Weidenbach |
Towards an Automatic Analysis of Security Protocols in First-Order Logic. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | E. Pascal Gribomont, Nachaat Salloum |
System Description: Using OBDD's for the validation of Skolem verification conditions. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Karsten Konrad, David A. Wolfram |
System Description: Kimba, A Model Generator for Many-Valued First-Order Logics. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Gopalan Nadathur, Dustin J. Mitchell |
System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Tobies |
A PSpace Algorithm for Graded Modal Logic. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Hillenbrand, Andreas Jaeger, Bernd Löchner |
System Description: Waldmeister - Improvements in Performance and Ease of Use. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Manfred Schmidt-Schauß, Klaus U. Schulz |
Solvability of Context Equations with Two Context Variables is Decidable. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Tomasz Wierzbicki |
Complexity of the higher order matching. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew A. Adams, Hanne Gottliebsen, Steve Linton, Ursula Martin |
VSDITLU: a verifiable symbolic definite integral table look-up. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Frank Pfenning, Carsten Schürmann |
System Description: Twelf - A Meta-Logical Framework for Deductive Systems. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Fuchs, Dirk Fuchs |
Abstraction-Based Relevancy Testing for Model Elimination. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner 0001, Norbert Eisinger, Ulrich Furbach |
A Confluent Connection Calculus. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrei Voronkov |
KK: a theorem prover for K. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandre Riazanov, Andrei Voronkov |
Vampire. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Dieter Hutter, Alan Bundy |
The Design of the CADE-16 Inductive Theorem Prover Contest. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Philippe de Groote |
A dynamic programming approach to categorial deduction. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthew Bishop |
A Breadth-First Strategy for Mating Search. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Baaz, Alexander Leitsch, Georg Moser |
System Description: CutRes 0.1: Cut Elimination by Resolution. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Prost |
A formalization of Static Analyses in System F. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Ullrich Hustadt, Renate A. Schmidt |
Maslov's Class K Revisited. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Sergei N. Artëmov |
On Explicit Reflection in Theorem Proving and Formal Verification. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Stéphane Demri, Rajeev Goré |
Tractable Transformations from Modal Provability Logics into First-Order Logic. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Harald Ganzinger (eds.) |
Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Nieuwenhuis |
Invited Talk: Rewrite-based Deduction and Symbolic Constraints. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller |
Extensional Higher-Order Paramodulation and RUE-Resolution. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Helmut Horacek |
Presenting Proofs in a Human-Oriented Way. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Stéphane Fèvre, Dongming Wang 0001 |
Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandre Boudet, Evelyne Contejean |
About the Confluence of Equational Pattern Rewrite Systems. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Claude Kirchner, Hélène Kirchner (eds.) |
Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Frank Pfenning |
Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller, Michael Kohlhase |
Extensional Higher-Order Resolution. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Karl Crary |
Admissibility of Fixpoint Induction over Partial Types. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernhard Beckert, Rajeev Goré |
System Description: leanK 2.0. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Beeson |
Unification in Lambda-Calculi with if-then-else. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Nonnengart, Georg Rock, Christoph Weidenbach |
On Generating Small Clause Normal Forms. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Reinhold Letz |
Using Matings for Pruning Connection Tableaux. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt |
System Description: card TAP: The First Theorem Prover on a Smart Card. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Tanel Tammet |
Towards Efficient Subsumption. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Jürgen Brauburger, Jürgen Giesl |
Termination Analysis by Inductive Evaluation. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa |
On the Relationship Between Non-Horn Magic Sets and Relevancy Testing. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthew Bishop, Peter B. Andrews |
Selectively Instantiating Definitions. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Leo Bachmair, Harald Ganzinger, Andrei Voronkov |
Elimination of Equality via Transformation with Ordering Constraints. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Hans Jürgen Ohlbach |
Combining Hilbert Style and Semantic Reasoning in a Resolution Framework. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Kreitz, Mark Hayden, Jason Hickey |
A Proof Environment for the Development of Group Communication Systems. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Arts, Mads Dam, Lars-Åke Fredlund, Dilian Gurov |
System Description: Verification of Distributed Erlang Programs. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy |
System Description: An Interface Between CLAM and HOL. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Julian Richardson, Alan Smaill, Ian Green |
System Description: Proof Planning in Higher-Order Logic with Lambda-Clam. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann |
ACL2 Support for Verification Projects (Invited Talk). |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Uwe Waldmann |
Superposition for Divisible Torsion-Free Abelian Groups. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Peltier |
System Description: An Equational Constraints Solver. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Robi Malik |
Automated Deduction of Finite-State Control Programs for Reactive Systems. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Bruno Pagano |
X.R.S : Explicit Reduction Systems - A First-Order Calculus for Higher-Order Calculi. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Laurent Théry |
A Certified Version of Buchberger's Algorithm. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph Douglas Horton, Bruce Spencer |
Rank/Activity: A Canonical Form for Binary Resolution. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Oliart, Wayne Snyder |
A Fast Algorithm for Uniform Semi-Unification. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques D. Fleuriot, Lawrence C. Paulson |
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Bertrand Mazure, Lakhdar Sais, Éric Grégoire |
System Description: CRIL Platform for SAT. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Fuchs, Andreas Wolf |
System Description: Cooperation in Model Elimination: CPTHEO. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller, Michael Kohlhase |
System Description: LEO - A Higher-Order Theorem Prover. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Hans de Nivelle |
A Resolution Decision Procedure for the Guarded Fragment. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Leo Bachmair, Harald Ganzinger |
Strict Basic Superposition. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Carsten Schürmann, Frank Pfenning |
Automated Theorem Proving in a Simple Meta-Logic for LF. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Fuchs |
System Description: Similarity-Based Lemma Generation for Model Elimination. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier 0002, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, Volker Sorge |
Omega: Towards a Mathematical Assistant. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Irène Durand, Aart Middeldorp |
Decidable Call by Need Computations in term Rewriting (Extended Abstract). |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Défourneaux, Nicolas Peltier |
Partial Matching for Analogy Discovery in Proofs and Counter-Examples. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Wolf 0005, Johann Schumann |
ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Moshe Y. Vardi |
Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel S. Korn, Christoph Kreitz |
Deciding Intuitionistic Propositional Logic via Translation into Classical Logic. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Johann Schumann |
Automatic Verification of Cryptographic Protocols with SETHEO. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Fuchs |
Evolving Combinators. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Hantao Zhang 0001 |
SATO: An Efficient Propositional Prover. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo |
Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Jürgen Ehrensberger, Claus Zinn |
DiaLog: A System for Dialogue Logic. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Dirk Fuchs, Matthias Fuchs |
CODE: A Powerful Prover for Problems of Condensed Detachment. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Mary Cryan, Allan Ramsay |
Constructing a Normal Form for Property Theory. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty, Douglas J. Howe |
Hybrid Interactive Theorem Proving Using Nuprl and HOL. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Jason J. Hickey |
Nuprl-Light: An Implementation Framework for Higher-Order Logics. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Uwe Egly |
Some Pitfalls of LK-to-LJ Translations and How to Avoid Them. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | David von Oheimb, Thomas F. Gritzner |
RALL: Machine-Supported Proofs for Relation Algebra. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
interactive and automatic theorem proving, atom structure, Relation algebra, Isabelle |
| 1 | Nikolaj S. Bjørner, Mark E. Stickel, Tomás E. Uribe |
A Practical Integration of First-Order Reasoning and Decision Procedures. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Koji Iwanuma |
Lemma Matching for a PTTP-based Top-down Theorem Prover. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani |
A New Method for Testing Decision Procedures in Modal Logics. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license