Search results for "CADE"

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

Publications at "CADE"( http://dblp.L3S.de/Venues/CADE )