Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | James Harland, David J. Pym |
Resource-Distribution via Boolean Constraint (Extended Abstract). |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant |
Proof Tactics for a Theory of State Machines in a Graphical Environment. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Kolbe, Jürgen Brauburger |
Plagiator - A Learning Prover. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt |
Connection-Based Proof Construction in Linear Logic. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Dieter Hutter, Michael Kohlhase |
A Colored Version of the Lambda-Calculus. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Wu Wen-Tsün |
The Char-Set Method and Its Applications to Automated Reasoning. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Franz Baader, Cesare Tinelli |
A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel |
Proving System Correctness with KIV 3.0. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | John K. Slaney |
Minlog: A Minimal Logic Theorem Prover. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Roussel, Philippe Mathieu |
Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | William McCune (eds.) |
Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Maris A. Ozols, Anthony Cant, Katherine A. Eastaughffe |
XIsabelle: A System Description. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Seán Matthews |
A Practical Implementation of Simple Consequence Relations Using Inductive Definitions. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Bernd I. Dahn, Jürgen Gehne, Th. Honigmann, Andreas Wolf |
Integration of Automated and Interactive Theorem Proving in ILP. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Richard Bornat, Bernard Sufrin |
Jape: A Calculator for Animating Proof-on-Paper. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Maria Paola Bonacina |
The Clause-Diffusion Theorem Prover Peers-mcd (System Description). |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Bernd Fischer 0002, Johann Schumann |
SETHEO Goes Software Engineering: Application of ATP to Software Reuse. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Helen Lowe, David Duncan |
XBarnacle: Making Theorem Provers More Accessible. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Joachim Niehren, Manfred Pinkal, Peter Ruhrberg |
On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
tree constraints, subtree relation, string unification, context unification, linear second-order unification, one-step rewriting, semantic processing of natural language |
1 | Lu Yang, Hongguang Fu, Zhenbing Zeng |
A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura |
Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Hans de Nivelle |
A Classification of Non-liftable Orders for Resolution. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Harald Ganzinger, Christoph Meyer 0001, Christoph Weidenbach |
Soft Typing for Ordered Resolution. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Mathias Kettner, Norbert Eisinger |
The Tableau Browser SNARKS. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Louise A. Dennis, Alan Bundy, Ian Green |
Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Sergei G. Vorobyov |
An Improved Lower Bound for the Elementary Theories of Trees. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Andrew Ireland, Alan Bundy |
Extensions to a Generalization Critic for Inductive Proof. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Qing Guo, Paliath Narendran, David A. Wolfram |
Unification and Matching Modulo Nilpotence. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
Subject area MECHANISMS, unification |
1 | Tobias Nipkow |
More Church-Rosser Proofs (in Isabelle/HOL). |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Boy de la Tour |
Ground Resolution with Group Computations on Semantic Symmetries. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema |
Transforming Termination by Self-Labelling. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Saturnino F. Luz-Filho |
Grammar Specification in Categorial Logics and Theorem Proving. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
Mechanisms (semantic tableaux) and Applications (computational liguistics) |
1 | Peter Graf |
Path Indexing for AC-Theories. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Christian B. Suttner, Geoff Sutcliffe |
The Design of the CADE-13 ATP System Competition. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Kolbe, Christoph Walther |
Termination of Theorem Proving by Reuse. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Wayne Snyder, James G. Schmolze |
Rewrite Semantics for Production Rule Systems: Theory and Applications. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Heribert Schütz, Tim Geisler |
Efficient Model Generation through Compilation. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Dana S. Scott |
What Can We Hope to Achieve From Automated Deduction? (Abstract). |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Giovanni Felici, Giovanni Rinaldi, Klaus Truemper |
FasTraC: A Decentralized Traffic Control System Based on Logic Programming. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Erica Melis, Jon Whittle 0001 |
Internal Analogy in Theorem Proving. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Konstantinos Sagonas, Terrance Swift, David Scott Warren |
An Abstract Machine for Fixed-Order Dynamically Stratified Programs. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang |
An Introduction to Geometry Expert. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Andrei Voronkov |
Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Martin Protzen |
Patching Faulty Conjectures. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | David Cyrluk, Patrick Lincoln, Natarajan Shankar |
On Shostak's Decision Procedure for Combinations of Theories. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Dieter Hutter, Claus Sengler |
INKA: The Next Generation. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Hans Jürgen Ohlbach |
SCAN - Elimination of Predicate Quantifiers. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Weidenbach, Bernd Gaede, Georg Rock |
SPASS & FLOTTER Version 0.42. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Tanel Tammet |
A Resolution Theorem Prover for Intuitonistic Logic. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Xiaorong Huang, Armin Fiedler |
Presenting Machine-Found Proofs. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Gernot Salzer |
Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Stephan Schmitt, Christoph Kreitz |
Converting Non-Classical Matrix Proofs into Sequent-Style Systems. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Peter Graf, Christoph Meyer 0001 |
Advanced Indexing Operations on Substitution Trees. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty |
Proof Search with Set Variable Instantiation in the Calculus of Constructions. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Janet Bertot, Yves Bertot |
CtCoq: A System Presentation. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
system presentation, Application |
1 | William M. Farmer, Joshua D. Guttman, F. Javier Thayer |
IMPS: An Updated System Description. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Torsten Schaub, Stefan Brüning, Pascal Nicolas |
XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Fuchs |
Experiments in the Heuristic Use of Past Proof Experience. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | David A. Basin, Seán Matthews |
Structuring Metatheory on Inductive Definitions. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Fausto Giunchiglia, Roberto Sebastiani |
Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Peter V. Homeier, David F. Martin |
Mechanical Verification of Mutually Recursive Procedures. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Jian Zhang 0001, Hantao Zhang 0001 |
System Description: Generating Models by SEM. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Uwe Egly, Thomas Rath |
On the Practical Value of Different Definitional Translations to Normal Form. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Optimizing Proof Search in Model Elimination. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Tai Joon Park, Allen Van Gelder |
Partitioning Methods for Satisfiability Testing on Large Formulas. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach |
MUltlog 1.0: Towards an Expert System for Many-Valued Logics. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Giuseppe De Giacomo, Fabio Massacci |
Tableaux and Algorithms for Propositional Dynamic Logic with Converse. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Michael A. McRobbie, John K. Slaney (eds.) |
Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Harald Ganzinger, Uwe Waldmann |
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Claus Sengler |
Termination of Algorithms over Non-freely Generated Data Types. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Dongming Wang 0001 |
GEOTHER: A Geometry Theorem Prover. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Steve Linton, Ursula Martin, Péter Pröhle, Duncan Shand |
Algebra and Automated Deduction. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Harald Ganzinger |
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Christian G. Fermüller |
Semantic Trees Revisited: Some New Completeness Results. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Miki Hermann, Phokion G. Kolaitis |
Unification Algorithms Cannot be Combined in Polynomial Time. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Nonnengart |
Resolution-Based Calculi for Modal and Temporal Logics. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Weidenbach |
Unification in Pseudo-Linear Sort Theories is Decidable. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Roussel, Philippe Mathieu |
A New Method for Knowledge Compilation: The Achievement by Cycle Search. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
expert systems, resolution, knowledge compilation |
1 | Ursula Martin |
Theorem Proving with Group Presentations: Examples and Questions. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Deepak Kapur, Mahadevan Subramaniam |
Lemma Discovery in Automated Induction. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Harald Rueß |
Reflection of Formal Tactics in a Deductive Reflection Framework. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Jörg Denzinger, Stephan Schulz 0001 |
Learning Domain Knowledge to Improve Theorem Proving. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Beckert, Reiner Hähnle, Peter Oel, Martin Sulzmann |
The Tableau-based Theorem Prover 3TAP Version 4.0. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Johann Schumann |
SiCoTHEO: Simple Competitive Parallel Theorem Provers. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Fausto Giunchiglia, Adolfo Villafiorita |
ABSFOL: A Proof Checker with Abstraction. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Clare Dixon |
Search Strategies for Resolution in Temporal Logics. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Eike Ritter, David J. Pym, Lincoln A. Wallen |
Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract). |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Ole Rasmussen |
An Embedding of Ruby in Isabelle. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | David A. McAllester, Kostas Arkoudas |
Walther Recursion. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Eric Domenjoud, Francis Klay, Christophe Ringeissen |
Combination Techniques for Non-Disjoint Equational Theories. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Penny Anderson |
Representing Proof Transformations for Program Optimizations. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Jian Zhang 0001 |
Problems on the Generation of Finite Models. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | John K. Slaney |
The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Edmund M. Clarke, Xudong Zhao 0005 |
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Goller, Reinhold Letz, Klaus Mayr, Johann Schumann |
SETHEO V3.2: Recent Developments - System Abstract. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Olav Lysne |
On the Connection between Narrowing and Proof by Consistency. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Peter Graf |
Extended Path-Indexing. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Beckert |
A Completion-Based Method for Mixed Universal and Rigid E-Unification. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Frank Pfenning |
Elf: A Meta-Language for Deductive Systems (System Descrition). |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Heng Chu, David A. Plaisted |
Semantically Guided First-Order Theorem Proving using Hyper-Linking. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|