CADE A

75 papers

YearTitle / Authors
1992&: Automated Natural Deduction.
Dave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill
1992A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract).
Daniel J. Dougherty, Patricia Johann
1992A Geometry Theorem Prover for Macintoshes.
Shang-Ching Chou
1992A Many Sorted Logic with Possibly Empty Sorts.
Anthony G. Cohn
1992A Natural Deduction Automated Theorem Proving System.
Li Dafa
1992A Normal Form for First-Order Temporal Formulae.
Michael Fisher
1992A Parallel Completion Procedure for Term Rewriting Systems.
Katherine A. Yelick, Stephen J. Garland
1992A Report in ICL HOL.
K. Blackburn
1992An Abstract View of Sorted Unification.
Alan M. Frisch, Anthony G. Cohn
1992An Improved Method for Adding Equality to Free Variable Semantic Tableaux.
Bernhard Beckert, Reiner Hähnle
1992An Interval-based Temporal Logic in a Multivalued Setting.
Mathias Bauer
1992An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems.
Tomás E. Uribe, Alan M. Frisch, Michael K. Mitchell
1992Analytica - A Theorem Prover in Mathematica.
Edmund M. Clarke, Xudong Zhao
1992Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor.
Robert S. Boyer, Yuan Yu
1992Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings
Deepak Kapur
1992Automatic Program Optimization Through Proof Transformation.
Peter Madden
1992Automatic Proofs in Mathematical Logic and Analysis.
Kurt Ammon
1992Basic Paramodulation and Superposition.
Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder
1992Benchmark Problems in Which Equality Plays the Major Role.
Ewing L. Lusk, Larry Wos
1992Caching and Lemmaizing in Model Elimination Theorem Provers.
Owen L. Astrachan, Mark E. Stickel
1992Computing Prime Implicates Incrementally.
Peter Jackson
1992Computing Transivity Tables: A Challenge For Automated Theorem Provers.
David A. Randell, Anthony G. Cohn, Zhan Cui
1992Cycle Unification.
Wolfgang Bibel, Steffen Hölldobler, Jörg Würtz
1992Decidable Matching for Convergent Systems (Preliminary Version).
Nachum Dershowitz, Subrata Mitra, G. Sivakumar
1992Difference Matching.
David A. Basin, Toby Walsh
1992Disproving Conjectures.
Martin Protzen
1992Embedding Negation as Failure into a Model Generation Theorem Prover.
Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa
1992Eves System Description.
Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, Mark Saaltink
1992Experiments in Automated Deduction with Condensed Detachment.
William McCune, Larry Wos
1992FRI: Failure-Resistant Induction in RRL.
Xin Hua, Hantao Zhang
1992Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors.
Delia Kesner
1992Grammar Rewriting.
David A. McAllester
1992Herky: High Performance Rewriting in RRL.
Hantao Zhang
1992IMPS: System Description.
William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1992Implementing the Meta-Theory of Deductive Systems.
Frank Pfenning, Ekkehard Rohwedder
1992Isabelle-91.
Tobias Nipkow, Lawrence C. Paulson
1992KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract).
Johann Schumann
1992LIM+ Challenge Problems by RUE Hyper-Resolution.
Vincent J. Digricoli, Eugene Kochendorfer
1992Linear-Input Subset Analysis.
Geoff Sutcliffe
1992Little Theories.
William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1992MGTP: A Parallel Theorem Prover Based on Lazy Model Generation.
Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita
1992One More Logic with Uncertainty and Resolution Principle for it.
Konstantin Vershinin, Igor Romanenko
1992PVS: A Prototype Verification System.
Sam Owre, John M. Rushby, Natarajan Shankar
1992Polynomial Interpretations and the Complexity of Algorithms.
Adam Cichon, Pierre Lescanne
1992Programming with Equations: A Framework for Lazy Parallel Evaluation.
R. C. Sekar, I. V. Ramakrishnan
1992Proof Search in the Intuitionistic Sequent Calculus.
Natarajan Shankar
1992Proving Equality Theorems with Hyper-Linking.
Geoffrey D. Alexander, David A. Plaisted
1992Proving Geometry Statements of Constructive Type.
Shang-Ching Chou, Xiao-Shan Gao
1992Proving the Chinese Remainder Theorem by the Cover Set Induction.
Hantao Zhang, Xin Hua
1992Puzzles and Paradoxes (Abstract).
Raymond M. Smullyan
1992ROO: A Parallel Theorem Prover.
Ewing L. Lusk, William McCune, John K. Slaney
1992RVF: An Automated Formal Verification System.
Tie-Cheng Wang, Allen Goldberg
1992Reduction and Unification in Lambda Calculi with Subtypes.
Tobias Nipkow, Zhenyu Qian
1992Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic.
Ricardo Caferra, Stéphane Demri
1992Some Termination Criteria for Narrowing and E-Narrowing.
Jim Christian
1992Sorted Unification Using Set Constraints.
Tomás E. Uribe
1992Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic.
Wilfred Z. Chen
1992The Central Variable Strategy of Str+ve.
Larry M. Hines
1992The FAUST - Prover.
Klaus Schneider, Ramayya Kumar, Thomas Kropf
1992The GAZER Theorem Prover.
Dave Barker-Plummer, Alex Rothenberg
1992The Impossibility of the Automation of Logical Reasoning.
Larry Wos
1992The KIV System: Systematic Construction of Verified Software.
Wolfgang Reif
1992The SHUNYATA System.
Kurt Ammon
1992The Semantically Guided Linear Deduction System.
Geoff Sutcliffe
1992The Special-Relation Rules are Incomplete.
Zohar Manna, Richard J. Waldinger
1992The Tableau-Based Theorem Prover
Bernhard Beckert, Stefan Gerberding, Reiner Hähnle, Werner Kernig
1992The Use of Proof Plans to Sum Series.
Toby Walsh, Alex Nunes, Alan Bundy
1992Theorem Proving in Non-Standard Logics Based on the Inverse Method.
Andrei Voronkov
1992Theorem Proving with Ordering Constrained Clauses.
Robert Nieuwenhuis, Albert Rubio
1992Theoretical Study of Symmetries in Propositional Calculus and Applications.
Belaid Benhamou, Lakhdar Sais
1992Unification in Order-Sorted Algebras with Overloading.
Alexandre Boudet
1992Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures.
Franz Baader, Klaus U. Schulz
1992Uniform Traversal Combinators: Definition, Use and Properties.
Leonidas Fegaras, Tim Sheard, David W. Stemple
1992Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs.
Jane Hesketh, Alan Bundy, Alan Smaill
1992Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker.
Jawahar Chirimar, Carl A. Gunter, Myra Van Inwegen