Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Martin Protzen |
Disproving Conjectures. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe |
Linear-Input Subset Analysis. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | K. Blackburn |
A Report in ICL HOL. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Shang-Ching Chou |
A Geometry Theorem Prover for Macintoshes. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Daniel J. Dougherty, Patricia Johann |
A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract). |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | David A. Randell, Anthony G. Cohn 0001, Zhan Cui |
Computing Transivity Tables: A Challenge For Automated Theorem Provers. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Hantao Zhang 0001 |
Herky: High Performance Rewriting in RRL. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Reif |
The KIV System: Systematic Construction of Verified Software. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Owen L. Astrachan, Mark E. Stickel |
Caching and Lemmaizing in Model Elimination Theorem Provers. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Jim Christian |
Some Termination Criteria for Narrowing and E-Narrowing. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf |
The FAUST - Prover. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Peter Madden |
Automatic Program Optimization Through Proof Transformation. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Peter Jackson |
Computing Prime Implicates Incrementally. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder |
Basic Paramodulation and Superposition. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | William M. Farmer, Joshua D. Guttman, F. Javier Thayer |
IMPS: System Description. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Ricardo Caferra, Stéphane Demri |
Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Edmund M. Clarke, Xudong Zhao 0005 |
Analytica - A Theorem Prover in Mathematica. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Alexandre Boudet |
Unification in Order-Sorted Algebras with Overloading. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | R. C. Sekar 0001, I. V. Ramakrishnan |
Programming with Equations: A Framework for Lazy Parallel Evaluation. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Delia Kesner |
Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Kurt Ammon |
The SHUNYATA System. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Hantao Zhang 0001, Xin Hua |
Proving the Chinese Remainder Theorem by the Cover Set Induction. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Robert Nieuwenhuis, Albert Rubio |
Theorem Proving with Ordering Constrained Clauses. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | William M. Farmer, Joshua D. Guttman, F. Javier Thayer |
Little Theories. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | William McCune, Larry Wos |
Experiments in Automated Deduction with Condensed Detachment. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Dave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill |
&: Automated Natural Deduction. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Vincent J. Digricoli, Eugene Kochendorfer |
LIM+ Challenge Problems by RUE Hyper-Resolution. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Konstantin Vershinin, Igor Romanenko |
One More Logic with Uncertainty and Resolution Principle for it. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Anthony G. Cohn 0001 |
A Many Sorted Logic with Possibly Empty Sorts. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Beckert, Reiner Hähnle |
An Improved Method for Adding Equality to Free Variable Semantic Tableaux. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | David A. Basin, Toby Walsh |
Difference Matching. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Frank Pfenning, Ekkehard Rohwedder |
Implementing the Meta-Theory of Deductive Systems. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Robert S. Boyer, Yuan Yu |
Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
Nqthm, Boyer-Moore Theorem Prover, Gnu, Ada, C, Automated reasoning, object code, formal program verification |
1 | Jawahar Chirimar, Carl A. Gunter, Myra Van Inwegen |
Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | David A. McAllester |
Grammar Rewriting. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita 0002 |
MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Jane Hesketh, Alan Bundy, Alan Smaill |
Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Johann Schumann |
KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract). |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
1 | Maritta Heisel, Wolfgang Reif, Werner Stephan 0001 |
Tactical Theorem Proving in Program Verification. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Dieter Hutter |
Guiding Induction Proofs. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Johann Schumann, Reinhold Letz, Franz J. Kurfess |
Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Paul Pritchard, John K. Slaney |
Tutorial on Computing Models of Propositional Logics. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | John K. Slaney, Ewing L. Lusk |
Parallelizing the Closure Computation in Automated Deduction. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Neil V. Murray, Erik Rosenthal |
DISSOLVER: A Dissolution-based Theorem Prover. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Frank Pfenning, Dan Nesmith |
Presenting Intuitive Deductions via Symmetric Simplification. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Ralph Butler, Ian T. Foster, Anita Jindal, Ross A. Overbeek |
A High-Performance Parallel Theorem Prover. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | John L. Pollock |
OSCAR. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Müller 0008, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka |
Tutorial on Reasoning and Representation with Concept Languages. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Toshiro Wakayama, T. H. Payne |
Case-Free Programs: An Abstraction of Definite Horn Programs. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Dan Benanav |
Simultaneous Paramodulation. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann |
RCL: A Lisp Verification System. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Newton C. A. da Costa, Lawrence J. Henschen, James J. Lu, V. S. Subrahmanian |
Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Frank M. Brown, Carlos Araya |
Cylindric Algebra Equation Solver. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Shang-Ching Chou, Xiao-Shan Gao |
Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
Wu's method, prover, elementary geometry, degenerate conditions, Ritt-Wu's principle, ascending chain, the dimension theorem, Morley's trisector theorem, ideal, mechanical theorem proving, algebraic variety |
1 | Amy P. Felty, Dale Miller 0001 |
Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Christian B. Suttner, Wolfgang Ertel |
Automatic Acquisition of Search Guiding Heuristics. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
learning, heuristics, features, Automated theorem proving, back-propagation, connectionism, evaluation functions, model elimination |
1 | Mark E. Stickel |
A Prolog Technology Theorem Prover. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Frank M. Brown, Carlos Araya |
Schemata. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Alan Bundy, Frank van Harmelen, Alan Smaill, Andrew Ireland |
Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Wayne Snyder |
Higher Order E-Unification. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Larry Wos, Steve Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler |
Automated Reasoning Contributed to Mathematics and Logic. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Alexandre Boudet |
Unification in a Combination of Equational Theories: an Efficient Algorithm. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Boy de la Tour |
Minimizing the Number of Clauses by Renaming. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe |
A General Clause Theorem Prover. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Ursula Martin, Tobias Nipkow |
Ordered Rewriting and Confluence. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | David A. Wolfram |
ACE: The Abstract Clause Engine. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Alan Bundy |
A Science of Reasoning: Extended Abstract. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Andrei Voronkov |
LISS - The Logic Inference Search System. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Leo Bachmair, Harald Ganzinger |
On Restrictions of Ordered Paramodulation with Simplification. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning |
The TPS Theorem Proving System. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Chitta Baral, Jorge Lobo 0001, Jack Minker |
Generalized Well-founded Semantics for Logic Programs (Extended Abstract). |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Jieh Hsiang, Jean-Pierre Jouannaud |
Tutorial on Rewrite-Based Theorem Proving. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Pierre Lescanne |
ORME: An Implementation of Completion Procedures as Sets of Transition Rules. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | William M. Farmer, Joshua D. Guttman, F. Javier Thayer |
IMPS: An Interactive Mathematical Proof System. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Bibel |
Perspectives on Automated Deduction (Abstract). |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Carl Eichenlaub, Bruce Esrig, James Hook, Carl Klapper, Garrel Pottinger |
The Romulus Proof Checker. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Yusuf Ozturk, Lawrence J. Henschen |
Hyper Resolution and Equality Axioms without Function Substitutions. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Sang Ho Lee, Lawrence J. Henschen |
Substitution-based Compilation of Extended Rules in Deductive Databases. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Masami Hagiya |
Programming by Example and Proving by Example Using Higher-order Unification. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Gerald E. Peterson |
Complete Sets of Reductions with Constraints. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Gramlich |
UNICOM: A Refined Completion Based Inductive Theorem Prover. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Mikael Rittri |
Retrieving Library Identifiers via Equational Matching of Types. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | William Pierce |
Toward Mechanical Methods for Streamlining Proofs. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Robert Nieuwenhuis, Fernando Orejas, Albert Rubio |
TRIP: An Implementation of Clausal Rewriting. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Larry M. Hines |
Str+ve-Subset: The Str+ve-based Subset Prover. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | David A. Basin |
Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty, Elsa L. Gunter, Dale Miller 0001, Frank Pfenning |
Tutorial on Lambda-Prolog. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Hans-Jürgen Bürckert |
A Resolution Principle for Clauses with Constraints. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Uday S. Reddy |
Term Rewriting Induction. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Joachim Steinbach |
Improving Assoviative Path Orderings. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | William McCune |
OTTER 2.0. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Robert S. Boyer, J Strother Moore |
A Theorem Prover for a Computational Logic. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Mark E. Stickel (eds.) |
10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Ewing L. Lusk, William McCune |
Tutorial on High-Performance Automated Theorem Proving. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Heikki Tuominen |
Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | David J. Pym, Lincoln A. Wallen |
Investigations into Proof-Search in a System of First-Order Dependent Function Types. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Richard J. Waldinger |
Tutorial on Program-Synthetic Deduction. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Hans Jürgen Ohlbach, Andreas Herzig |
Tutorial on Compilation techniques for Logics. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Alan F. McMichael |
SLIM: An Automated Reasoner For Equivalences, Applied To Set Theory. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Daniel J. Dougherty, Patricia Johann |
An Improved General E-Unification Method. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|