Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Robert S. Boyer |
Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We? |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Rolf Socher-Ambrosius |
A Refined Version of General E-Unification. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Jacques Chazarain, Emmanuel Kounalis |
Mechanizable Inductive Proofs for a Class of Forall Exists Formulas. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Jean Goubault |
Proving with BDDs and Control of Information. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Siani Baker |
A New Application for Explanation-Based Generalisation within Automated Deduction. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | D. Andre de Waal, John P. Gallagher |
The Applicability of Logic Program Analysis and Transformation to Theorem Proving. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Koji Iwanuma |
Conservative Query Normalization on Parallel Circumscription. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Larry M. Hines |
Str+ve and Integers. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Takeshi Ohtani, Hajime Sawamura, Toshiro Minami |
EUODHILOS-II on Top of GNU Epoch. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Beckert, Joachim Posegga |
leanTAP: Lean Tableau-Based Theorem Proving (Extended Abstract). |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | David A. Basin, Toby Walsh |
Termination Orderings for Rippling. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Lawrence C. Paulson |
A Fixedpoint Approach to Implementing (Co)Inductive Definitions. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty, Douglas J. Howe |
Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Christophe Bourely, Ricardo Caferra, Nicolas Peltier |
A Method for Building Models Automatically. Experiments with an Extension of OTTER. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Véronique Royer, Joachim Quantz |
On Intuitionistic Query Answering in Description Bases. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
Intuitionistic Sequent Calculus, Least Fixed Point Semantics, Description Logics, Query Answering |
1 | Christian Prehofer |
Decidable Higher-Order Unification Problems. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Manfred Kerber, Michael Kohlhase |
A Mechanization of Strong Kleene Logic for Partial Functions. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Gernot Salzer |
Primal Grammars and Unification Modulo a Binary Clause. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Lars-Henrik Eriksson |
Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Xiaorong Huang |
Reconstruction Proofs at the Assertion Level. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Claus-Peter Wirth, Bernhard Gramlich |
On Notions of Inductive Validity for First-Oder Equational Clauses. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Martin Protzen |
Lazy Generation of Induction Hypotheses. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Dongming Wang 0001 |
Algebraic Factoring and Geometry Proving. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Ursula Martin |
Termination, Geometry and Invariants. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Johann Schumann |
DELTA - A Bottom-up Preprocessor for Top-Down Theorem Provers - System Abstract. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | anonymous |
The QED Manifesto. |
CADE |
1994 |
DBLP BibTeX RDF |
|
1 | Frederic D. Portoraro |
Symlog: Automated Advice in Fitch-style Proof Construction. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann |
KEIM: A Toolkit for Automated Deduction. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Maria Paola Bonacina, William McCune |
Distributed Theorem Proving by Peers. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Adel Bouhoula |
SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Robert Nieuwenhuis, Albert Rubio |
AC-Superposition with Constraints: No AC-Unifiers Needed. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Fabio Massacci |
Strongly Analytic Tableaux for Normal Modal Logics. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Laurent Fribourg, Marcos Veloso Peixoto |
Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001, Ulrich Furbach |
Model Elimination Without Contrapositives. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | William M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer |
Proof Script Pragmatics in IMPS. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Patricia Johann, Michael Kohlhase |
Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | François Bronsard, Uday S. Reddy, Robert W. Hasker |
Induction using Term Orderings. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Toby Walsh |
A Divergence Critic. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Paul B. Jackson |
Exploring Abstract Algebra in Constructive Type Theory. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann |
Omega-MKRP: A Proof Development Environment. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Miki Hermann, Phokion G. Kolaitis |
The Complexity of Counting Problems in Equational Matching. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Tie-Cheng Wang, Allen Goldberg |
KITP-93: An Automated Inference System for Program Analysis. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Leo Bachmair, Harald Ganzinger |
Ordered Chaining for Total Orderings. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Aart Middeldorp, Hans Zantema |
Simple Termination Revisited. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe, Christian B. Suttner, Theodor Yemenis |
The TPTP Problem Library. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001, Ulrich Furbach |
PROTEIN: A PROver with a Theory Extension INterface. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | David A. Plaisted |
The Search Efficiency of Theorem Proving Strategies. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | John K. Slaney |
FINDER: Finite Domain Enumerator - System Description. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Richard Platek |
What is a Proof? (Abstract). |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Brüning |
Detecting Non-Provable Goals. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Alan Bundy (eds.) |
Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Laurent Vigneron |
Associative-Commutative Deduction with Constraints. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Robert L. Constable |
Exporting and Refecting Abstract Metamathematics. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Nicholas Freitag McPhee, Shang-Ching Chou, Xiao-Shan Gao |
Mechanically Proving Geometry Theorems Using a Combination of Wu's Method and Collins' Method. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Reinhard Bündgen |
On Pot, Pans and Pudding or How to Discover Generalised Critical Pairs. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | David B. Sturgill, Alberto Maria Segre |
A Novel Asynchronous Parallelism Scheme for First-Order Logic. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Klingenbeck, Reiner Hähnle |
Semantic Tableaux with Ordering Restrictions. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Bradley L. Richards, Ina Kraan, Alan Smaill, Geraint A. Wiggins |
Mollusc: A General Proof-Development Shell for Sequent-Based Logics. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Bibel, Stefan Brüning, Uwe Egly, Thomas Rath |
KoMeT. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Olaf Müller, Franz Weber |
Theory and Practice of Minimal Modular Higher-Order E-Unification. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | John K. Slaney, Ewing L. Lusk, William McCune |
SCOTT: Semantically Constrained Otter System Description. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Dieter Hutter |
Synthesis of Induction Orderings for Existence Proofs. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood |
Deductive Composition of Astronomical Software from Subroutine Libraries. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Adam Cichon, Pierre Lescanne |
Polynomial Interpretations and the Complexity of Algorithms. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Shang-Ching Chou, Xiao-Shan Gao |
Proving Geometry Statements of Constructive Type. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
Geometry theorem proving, Wu's method, non-degenerate condition, generally true, constructive geometry statement, metric geometry, algebraically closed field, Euclidean geometry |
1 | Kurt Ammon |
Automatic Proofs in Mathematical Logic and Analysis. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Tomás E. Uribe |
Sorted Unification Using Set Constraints. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Bibel, Steffen Hölldobler, Jörg Würtz |
Cycle Unification. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Franz Baader, Klaus U. Schulz |
Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Zohar Manna, Richard J. Waldinger |
The Special-Relation Rules are Incomplete. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Deepak Kapur (eds.) |
Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Tie-Cheng Wang, Allen Goldberg |
RVF: An Automated Formal Verification System. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, Mark Saaltink |
Eves System Description. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Andrei Voronkov |
Theorem Proving in Non-Standard Logics Based on the Inverse Method. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Tobias Nipkow, Lawrence C. Paulson |
Isabelle-91. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Raymond M. Smullyan |
Puzzles and Paradoxes (Abstract). |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Toby Walsh, Alex Nunes, Alan Bundy |
The Use of Proof Plans to Sum Series. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Wilfred Z. Chen |
Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Xin Hua, Hantao Zhang 0001 |
FRI: Failure-Resistant Induction in RRL. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Nachum Dershowitz, Subrata Mitra, G. Sivakumar |
Decidable Matching for Convergent Systems (Preliminary Version). |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa |
Embedding Negation as Failure into a Model Generation Theorem Prover. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Li Dafa |
A Natural Deduction Automated Theorem Proving System. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Larry M. Hines |
The Central Variable Strategy of Str+ve. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Larry Wos |
The Impossibility of the Automation of Logical Reasoning. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Geoffrey D. Alexander, David A. Plaisted |
Proving Equality Theorems with Hyper-Linking. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Ewing L. Lusk, Larry Wos |
Benchmark Problems in Which Equality Plays the Major Role. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Alan M. Frisch, Anthony G. Cohn 0001 |
An Abstract View of Sorted Unification. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Michael Fisher 0001 |
A Normal Form for First-Order Temporal Formulae. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Katherine A. Yelick, Stephen J. Garland |
A Parallel Completion Procedure for Term Rewriting Systems. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Mathias Bauer |
An Interval-based Temporal Logic in a Multivalued Setting. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Dave Barker-Plummer, Alex Rothenberg |
The GAZER Theorem Prover. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Beckert, Stefan Gerberding, Reiner Hähnle, Werner Kernig |
The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Tobias Nipkow, Zhenyu Qian |
Reduction and Unification in Lambda Calculi with Subtypes. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe |
The Semantically Guided Linear Deduction System. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Leonidas Fegaras, Tim Sheard, David W. Stemple |
Uniform Traversal Combinators: Definition, Use and Properties. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Ewing L. Lusk, William McCune, John K. Slaney |
ROO: A Parallel Theorem Prover. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Tomás E. Uribe, Alan M. Frisch, Michael K. Mitchell |
An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Natarajan Shankar |
Proof Search in the Intuitionistic Sequent Calculus. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Belaid Benhamou, Lakhdar Sais |
Theoretical Study of Symmetries in Propositional Calculus and Applications. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Sam Owre, John M. Rushby, Natarajan Shankar |
PVS: A Prototype Verification System. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|