CADE A

74 papers

YearTitle / Authors
1994A Completion-Based Method for Mixed Universal and Rigid E-Unification.
Bernhard Beckert
1994A Divergence Critic.
Toby Walsh
1994A Fixedpoint Approach to Implementing (Co)Inductive Definitions.
Lawrence C. Paulson
1994A Mechanization of Strong Kleene Logic for Partial Functions.
Manfred Kerber, Michael Kohlhase
1994A Method for Building Models Automatically. Experiments with an Extension of OTTER.
Christophe Bourely, Ricardo Caferra, Nicolas Peltier
1994A New Application for Explanation-Based Generalisation within Automated Deduction.
Siani Baker
1994A Novel Asynchronous Parallelism Scheme for First-Order Logic.
David B. Sturgill, Alberto Maria Segre
1994A Refined Version of General E-Unification.
Rolf Socher-Ambrosius
1994AC-Superposition with Constraints: No AC-Unifiers Needed.
Robert Nieuwenhuis, Albert Rubio
1994Algebraic Factoring and Geometry Proving.
Dongming Wang
1994Associative-Commutative Deduction with Constraints.
Laurent Vigneron
1994Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings
Alan Bundy
1994Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints.
Laurent Fribourg, Marcos Veloso Peixoto
1994Combination Techniques for Non-Disjoint Equational Theories.
Eric Domenjoud, Francis Klay, Christophe Ringeissen
1994Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan.
Edmund M. Clarke, Xudong Zhao
1994Conservative Query Normalization on Parallel Circumscription.
Koji Iwanuma
1994DELTA - A Bottom-up Preprocessor for Top-Down Theorem Provers - System Abstract.
Johann Schumann
1994Decidable Higher-Order Unification Problems.
Christian Prehofer
1994Deductive Composition of Astronomical Software from Subroutine Libraries.
Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood
1994Detecting Non-Provable Goals.
Stefan Brüning
1994Distributed Theorem Proving by Peers.
Maria Paola Bonacina, William McCune
1994EUODHILOS-II on Top of GNU Epoch.
Takeshi Ohtani, Hajime Sawamura, Toshiro Minami
1994Elf: A Meta-Language for Deductive Systems (System Descrition).
Frank Pfenning
1994Exploring Abstract Algebra in Constructive Type Theory.
Paul B. Jackson
1994Exporting and Refecting Abstract Metamathematics.
Robert L. Constable
1994Extended Path-Indexing.
Peter Graf
1994FINDER: Finite Domain Enumerator - System Description.
John K. Slaney
1994Induction using Term Orderings.
François Bronsard, Uday S. Reddy, Robert W. Hasker
1994KEIM: A Toolkit for Automated Deduction.
Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann
1994KITP-93: An Automated Inference System for Program Analysis.
Tie-Cheng Wang, Allen Goldberg
1994KoMeT.
Wolfgang Bibel, Stefan Brüning, Uwe Egly, Thomas Rath
1994Lazy Generation of Induction Hypotheses.
Martin Protzen
1994Mechanically Proving Geometry Theorems Using a Combination of Wu's Method and Collins' Method.
Nicholas Freitag McPhee, Shang-Ching Chou, Xiao-Shan Gao
1994Mechanizable Inductive Proofs for a Class of Forall Exists Formulas.
Jacques Chazarain, Emmanuel Kounalis
1994Model Elimination Without Contrapositives.
Peter Baumgartner, Ulrich Furbach
1994Mollusc: A General Proof-Development Shell for Sequent-Based Logics.
Bradley L. Richards, Ina Kraan, Alan Smaill, Geraint A. Wiggins
1994Omega-MKRP: A Proof Development Environment.
Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann
1994On Intuitionistic Query Answering in Description Bases.
Véronique Royer, Joachim Quantz
1994On Notions of Inductive Validity for First-Oder Equational Clauses.
Claus-Peter Wirth, Bernhard Gramlich
1994On Pot, Pans and Pudding or How to Discover Generalised Critical Pairs.
Reinhard Bündgen
1994On the Connection between Narrowing and Proof by Consistency.
Olav Lysne
1994Ordered Chaining for Total Orderings.
Leo Bachmair, Harald Ganzinger
1994PROTEIN: A PROver with a Theory Extension INterface.
Peter Baumgartner, Ulrich Furbach
1994Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We?
Robert S. Boyer
1994Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions.
Lars-Henrik Eriksson
1994Primal Grammars and Unification Modulo a Binary Clause.
Gernot Salzer
1994Problems on the Generation of Finite Models.
Jian Zhang
1994Proof Script Pragmatics in IMPS.
William M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer
1994Proving with BDDs and Control of Information.
Jean Goubault
1994Reconstruction Proofs at the Assertion Level.
Xiaorong Huang
1994Representing Proof Transformations for Program Optimizations.
Penny Anderson
1994SCOTT: Semantically Constrained Otter System Description.
John K. Slaney, Ewing L. Lusk, William McCune
1994SETHEO V3.2: Recent Developments - System Abstract.
Christoph Goller, Reinhold Letz, Klaus Mayr, Johann Schumann
1994SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs.
Adel Bouhoula
1994Semantic Tableaux with Ordering Restrictions.
Stefan Klingenbeck, Reiner Hähnle
1994Semantically Guided First-Order Theorem Proving using Hyper-Linking.
Heng Chu, David A. Plaisted
1994Simple Termination Revisited.
Aart Middeldorp, Hans Zantema
1994Str+ve and Integers.
Larry M. Hines
1994Strongly Analytic Tableaux for Normal Modal Logics.
Fabio Massacci
1994Symlog: Automated Advice in Fitch-style Proof Construction.
Frederic D. Portoraro
1994Synthesis of Induction Orderings for Existence Proofs.
Dieter Hutter
1994Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables.
Amy P. Felty, Douglas J. Howe
1994Termination Orderings for Rippling.
David A. Basin, Toby Walsh
1994Termination, Geometry and Invariants.
Ursula Martin
1994The Applicability of Logic Program Analysis and Transformation to Theorem Proving.
D. Andre de Waal, John P. Gallagher
1994The Complexity of Counting Problems in Equational Matching.
Miki Hermann, Phokion G. Kolaitis
1994The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure.
John K. Slaney
1994The QED Manifesto.
anonymous
1994The Search Efficiency of Theorem Proving Strategies.
David A. Plaisted
1994The TPTP Problem Library.
Geoff Sutcliffe, Christian B. Suttner, Theodor Yemenis
1994Theory and Practice of Minimal Modular Higher-Order E-Unification.
Olaf Müller, Franz Weber
1994Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading.
Patricia Johann, Michael Kohlhase
1994What is a Proof? (Abstract).
Richard Platek
1994leanT
Bernhard Beckert, Joachim Posegga