Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Werner Nutt |
Unification in Monoidal Theories. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Käufl, Nicolas Zabel |
The Theorem Prover of the Program Verifier Tatzelwurm. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Alan Bundy, Frank van Harmelen, Christian Horn, Alan Smaill |
The Oyster-Clam System. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Franz Baader |
Rewrite Systems for Varieties of Semigroups. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Mark Tarver |
An Examination of the Prolog Technology Theorem-Prover. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
PTTP, metalevel reasoning, Prolog Normal Form, refinement |
1 | Paliath Narendran, Friedrich Otto |
Some Results on Equational Unification. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Camilla Schwind |
A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Ronald W. Satz |
EXPERT THINKER: An Adaptation of F-Prolog to Microcomputers. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Claude Kirchner |
Tutorial on Equational Unification. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | James A. Altucher, Prakash Panangaden |
A Mechanically Assisted Constructive Proof in Category Theory. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Peter Jackson, John Pais |
Computing Prime Implicants. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Xumin Nie, David A. Plaisted |
A Complete Semantic Back Chaining Proof System. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
1 | Johann Schumann, Reinhold Letz |
PARTHEO: A High-Performance Parallel Theorem Prover. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
Warren Abstract Machine, message passing, Theorem proving, first-order logic, transputers, or-parallelism, model elimination, connection method |
1 | Richard C. Potter, David A. Plaisted |
Term Rewriting: Some Experimental Results. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
Theorem proving, set theory, term rewriting |
1 | Timothy Griffin |
EFS - An Interactive Environment for Formal Systems. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Ralph Butler, Rasiah Loganantharaj, Robert Olson |
Notes on Prolog Program Transformations, Prolog Style, and Efficient Compilation to The Warren Abstract Machine. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Frank M. Brown, Seung S. Park, Jim Phelps |
ZPLAN: An Automatic Reasoning System for Situations. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | V. S. Subrahmanian, Zerksis D. Umrigar |
QUANTLOG: A System for Approximate Reasoning in Inconsistent Formal Systems. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Bishop Brock, Shaun Cooper, William Pierce |
Analogical Reasoning and Proof Discovery. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | D. Duchier, Drew V. McDermott |
LOGICALC: An Environment for Interactive Proof Development. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade |
Some Tools for an Inference Laboratory (ATINF). |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Walther |
Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Lawrence C. Paulson |
Isabelle: The Next Seven Hundred Theorem Provers. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Louise E. Moser |
A Decision Procedure for Unquantified Formulas of Graph Theory. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
congruence closure, equivalence class representative, Directed graph, decision procedure, normal form |
1 | David Cyrluk, Richard M. Harris, Deepak Kapur |
GEOMETER: A Theorem Prover for Algebraic Geometry. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Patrick Lincoln, Jim Christian |
Adventures in Associative-Commutative Unification (A Summary). |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Donald Simon |
Checking Natural Language Proofs. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar |
Canonical Conditional Rewrite Systems. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | William McCune |
Challenge Equality Problems in Lattice Theory. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Hantao Zhang 0001, Deepak Kapur |
First-Order Theorem Proving Using Conditional Rewrite Rules. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Douglas J. Howe |
Computational Metatheory in Nuprl. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
formal metamathematics, reflection, Theorem proving, type theory, constructive mathematics, tactics |
1 | Rakesh M. Verma, I. V. Ramakrishnan |
Optimal Time Bounds for Parallel Term Matching. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
optimal bounds, parallel term matching, complexity |
1 | David A. Plaisted |
A Goal Directed Theorem Prover. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Mark E. Stickel |
The KLAUS Automated Deduction System. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Rolf Socher |
A Subsumption Algorithm Based on Characteristic Matrices. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning |
The TPS Theorem Proving System. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Mehmet Dincbas, Pascal Van Hentenryck, Helmut Simonis, Abderrahmane Aggoun, Alexander Herold |
The CHIP System: Constraint Handling In Prolog. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Wolfram Büttner |
Unification in Finite Algebras is Unitary (?). |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | David A. Basin |
An Environment For Automated Reasoning About Partial Functions. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
Automated program development, unsolvability, theorem proving, computability, type theory, constructivity, tactics, partial functions |
1 | P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov |
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Hantao Zhang 0001, Deepak Kapur, Mukkai S. Krishnamoorthy |
A Mechanizable Induction Principle for Equational Specifications. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Frank M. Brown, Seung S. Park |
SYMEVAL: A Theorem Prover Based on the Experimental Logic. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Deepak Kapur, Hantao Zhang 0001 |
RRL: A Rewrite Rule Laboratory. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller 0001, Gopalan Nadathur, Andre Scedrov |
Lambda-Prolog: An Extended Logic Programming Language. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Ilkka Niemelä |
Decision Procedure for Autoepistemic Logic. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
analytic tableaux, theorem proving, Nonmonotonic logic |
1 | David A. McAllester |
Ontic: A Knowledge Representation System for Mathematics. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder |
Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Peter K. Malkin, Errol P. Martin |
Logical Matrix Generation and Testing. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Bruce T. Smith, Donald W. Loveland |
An nH-Prolog Implementation. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Hans-Jürgen Bürckert |
Solving Disequations in Equational Theories. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
E-unification, E-disunification, solving equations and disequations, Equational theories |
1 | Neil V. Murray, Erik Rosenthal |
An Implementation of a Dissolution-Based System Employing Theory Links. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Frank Pfenning |
Single Axioms in the Implicational Propositional Calculus. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Toshiro Wakayama, T. H. Payne |
Case Inference in Resolution-Based Languages. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Ewing L. Lusk, Ross A. Overbeek (eds.) |
9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Mark E. Stickel |
A Prolog Technology Theorem Prover. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Karl-Hans Bläsius, Jörg H. Siekmann |
Partial Unification for Graph Based Equational Reasoning. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
built-in equality, clause graphs with equality, planning in abstraction spaces, Unification |
1 | Arkady Rabinov |
A Restriction of Factoring in Binary Resolution. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
binary resolution, theorem proving, Factoring |
1 | Michael A. McRobbie, Robert K. Meyer, Paul B. Thistlewaite |
Towards Efficient "Knowledge-Based" Automated Theorem Proving for Non-Standard Logics. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Pierre Bieber, Luis Fariñas del Cerro, Andreas Herzig |
MOLOG: a Modal PROLOG. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Maritta Heisel, Wolfgang Reif, Werner Stephan 0001 |
Implementing Verification Strategies in the KIV-System. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Alan Bundy |
The Use of Explicit Plans to Guide Inductive Proofs. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
inductive proofs, formal methods, planning, theorem proving, automatic programming, Proof plans |
1 | Rainer Manthey, François Bry |
SATCHMO: A Theorem Prover Implemented in Prolog. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Leo Marcus, Timothy Redmond |
Two Automated Methods in Implementation Proofs. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
microcode verification, implementation, program verification, Program correctness |
1 | V. S. Subrahmanian |
Query Processing in Quantitative Logic Programming. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Jack Minker, Arcot Rajasekar |
Procedural Interpretation of Non-Horn Logic Programs. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
generalized closed world assumption, non-horn programs, procedural interpretation, support-for-negation, logic programming, negation |
1 | Emmanuel Kounalis, Michaël Rusinowitch |
On Word Problems in Horn Theories. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
initial model, inductionless induction, resolution, term-rewriting system, Horn clause, word problems |
1 | Larry M. Hines |
Hyper-Chaining and Knowledge-Based Theorem Proving. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Tie-Cheng Wang |
Elements of Z-Module Reasoning. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Philippe Besnard, Pierre Siegel |
Supposition-Based Logic for Automated Nonmontonic Reasoning. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Käufl |
Reasoning about Systems of Linear Inequalities. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Michael R. Donat, Lincoln A. Wallen |
Learning and Applying Generalised Solutions using Higher Order Resolution. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
higher order unification, Resolution, generalisation, Explanation Based Learning |
1 | Hans Jürgen Ohlbach |
A Resolution Calculus for Modal Logics. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
resolution principle, modal logic, unification |
1 | Mark Franzen, Lawrence J. Henschen |
A New Approach to Universal Unification and Its Application to AC-Unification. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Bill Pase, Sentot Kromodimoeljo |
m-NEVER System Summary. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
Automatic induction, forward rules, program verification, decision procedures, interactive theorem proving, rewrite rules |
1 | A. A. Aaby, K. T. Narayana |
Propositional Temporal Interval Logic is PSPACE Complete. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Marc Bezem |
Consistency of Rule-based Expert System. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
& Phrases knowledge-based systems, knowledge representation, consistency, rule-based expert systems |
1 | Manfred Schmidt-Schauß |
Unification in a Combination of Arbitrary Disjoint Equational Theories. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
Decidability of Unification, Combination of equational theories, Boolean rings, Unification, Equational theories, Abelian groups |
1 | Rick L. Stevens |
Challenge Problems from Nonassociative Rings for Theorem Provers. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Stephen J. Garland, John V. Guttag |
LP: The Larch Prover. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty, Dale Miller 0001 |
Specifying Theorem Provers in a Higher-Order Logic Programming Language. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Ralph Butler, Nicholas T. Karonis |
Exploitation of Parallelism in Prototypical Deduction Problems. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Shan Chi, Lawrence J. Henschen |
Recursive Query Answering with Non-Horn Clauses. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Luis Fariñas del Cerro, Andreas Herzig |
Linear Modal Deductions. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann |
An Interactive Enhancement to the Boyer-Moore Theorem Prover. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | H. Azzoune |
Type Inference in Prolog. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
Prolog, Type, Type Inference |
1 | Paul Jacquet |
Program Synthesis by Completion with Dependent Subtypes. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
Conditional and Order Sorted Rewriting, Program Synthesis |
1 | Larry Wos, William McCune |
Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Beierle, Walter G. Olthoff, Angi Voß |
Automatic Theorem Proving in the ISDV System. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Sara Porat, Nissim Francez |
Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Norbert Eisinger |
What You Always Wanted to Know About Clause Graph Resolution. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
Clause Graphs, Completeness, Strategies, Resolution, Confluence, Connection Graphs |
1 | Norbert Eisinger, Hans Jürgen Ohlbach |
The Markgraf Karl Refutation Procedure (MKRP). |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Gérard P. Huet |
Mechanizing Constructive Proofs (Abstract). |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Steven Greenbaum, David A. Plaisted |
The Illinois Prover: A General Purpose Resolution Theorem Prover. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Roland Dietrich |
Relating Resolution and Algebraic Completion for Horn Logic. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Hans-Albert Schneider |
An Improvement of Deduction Plans: Refutation Plans. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Hubert Comon |
Sufficient Completness, Term Rewriting Systems and "Anti-Unification". |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Gérard P. Huet |
Theorem Proving Systems of the Formel Project. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | David A. Plaisted |
A Simple Non-Termination Test for the Knuth-Bendix Method. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Mark E. Stickel |
A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
1 | Philip T. Cox, Tomasz Pietrzykowski |
Causes for Events: Their Computation and Applications. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|