Conferences in DBLP
Larry Wos The Impossibility of the Automation of Logical Reasoning. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:1-3 [Conf ] Kurt Ammon Automatic Proofs in Mathematical Logic and Analysis. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:4-19 [Conf ] Shang-Ching Chou , Xiao-Shan Gao Proving Geometry Statements of Constructive Type. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:20-34 [Conf ] Larry M. Hines The Central Variable Strategy of Str+ve. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:35-49 [Conf ] Franz Baader , Klaus U. Schulz Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:50-65 [Conf ] Tobias Nipkow , Zhenyu Qian Reduction and Unification in Lambda Calculi with Subtypes. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:66-78 [Conf ] Daniel J. Dougherty , Patricia Johann A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract). [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:79-93 [Conf ] Wolfgang Bibel , Steffen Hölldobler , Jörg Würtz Cycle Unification. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:94-108 [Conf ] Katherine A. Yelick , Stephen J. Garland A Parallel Completion Procedure for Term Rewriting Systems. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:109-123 [Conf ] David A. McAllester Grammar Rewriting. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:124-138 [Conf ] Adam Cichon , Pierre Lescanne Polynomial Interpretations and the Complexity of Algorithms. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:139-147 [Conf ] Leonidas Fegaras , Tim Sheard , David W. Stemple Uniform Traversal Combinators: Definition, Use and Properties. [Citation Graph (2, 0)][DBLP ] CADE, 1992, pp:148-162 [Conf ] Tomás E. Uribe Sorted Unification Using Set Constraints. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:163-177 [Conf ] Alan M. Frisch , Anthony G. Cohn An Abstract View of Sorted Unification. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:178-192 [Conf ] Alexandre Boudet Unification in Order-Sorted Algebras with Overloading. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:193-207 [Conf ] Raymond M. Smullyan Puzzles and Paradoxes (Abstract). [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:208- [Conf ] William McCune , Larry Wos Experiments in Automated Deduction with Condensed Detachment. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:209-223 [Conf ] Owen L. Astrachan , Mark E. Stickel Caching and Lemmaizing in Model Elimination Theorem Provers. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:224-238 [Conf ] Vincent J. Digricoli , Eugene Kochendorfer LIM+ Challenge Problems by RUE Hyper-Resolution. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:239-252 [Conf ] Peter Jackson Computing Prime Implicates Incrementally. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:253-267 [Conf ] Geoff Sutcliffe Linear-Input Subset Analysis. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:268-280 [Conf ] Belaid Benhamou , Lakhdar Sais Theoretical Study of Symmetries in Propositional Calculus and Applications. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:281-294 [Conf ] David A. Basin , Toby Walsh Difference Matching. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:295-309 [Conf ] Jane Hesketh , Alan Bundy , Alan Smaill Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:310-324 [Conf ] Toby Walsh , Alex Nunes , Alan Bundy The Use of Proof Plans to Sum Series. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:325-339 [Conf ] Martin Protzen Disproving Conjectures. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:340-354 [Conf ] Mathias Bauer An Interval-based Temporal Logic in a Multivalued Setting. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:355-369 [Conf ] Michael Fisher A Normal Form for First-Order Temporal Formulae. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:370-384 [Conf ] Ricardo Caferra , Stéphane Demri Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:385-399 [Conf ] Katsumi Inoue , Miyuki Koshimura , Ryuzo Hasegawa Embedding Negation as Failure into a Model Generation Theorem Prover. [Citation Graph (1, 0)][DBLP ] CADE, 1992, pp:400-415 [Conf ] Robert S. Boyer , Yuan Yu Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:416-430 [Conf ] Hantao Zhang , Xin Hua Proving the Chinese Remainder Theorem by the Cover Set Induction. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:431-445 [Conf ] Peter Madden Automatic Program Optimization Through Proof Transformation. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:446-460 [Conf ] Leo Bachmair , Harald Ganzinger , Christopher Lynch , Wayne Snyder Basic Paramodulation and Superposition. [Citation Graph (1, 0)][DBLP ] CADE, 1992, pp:462-476 [Conf ] Robert Nieuwenhuis , Albert Rubio Theorem Proving with Ordering Constrained Clauses. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:477-491 [Conf ] Zohar Manna , Richard J. Waldinger The Special-Relation Rules are Incomplete. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:492-506 [Conf ] Bernhard Beckert , Reiner Hähnle An Improved Method for Adding Equality to Free Variable Semantic Tableaux. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:507-521 [Conf ] Natarajan Shankar Proof Search in the Intuitionistic Sequent Calculus. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:522-536 [Conf ] Frank Pfenning , Ekkehard Rohwedder Implementing the Meta-Theory of Deductive Systems. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:537-551 [Conf ] Wilfred Z. Chen Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:552-566 [Conf ] William M. Farmer , Joshua D. Guttman , F. Javier Thayer Little Theories. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:567-581 [Conf ] Jim Christian Some Termination Criteria for Narrowing and E-Narrowing. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:582-588 [Conf ] Nachum Dershowitz , Subrata Mitra , G. Sivakumar Decidable Matching for Convergent Systems (Preliminary Version). [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:589-602 [Conf ] Delia Kesner Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:603-617 [Conf ] R. C. Sekar , I. V. Ramakrishnan Programming with Equations: A Framework for Lazy Parallel Evaluation. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:618-632 [Conf ] Anthony G. Cohn A Many Sorted Logic with Possibly Empty Sorts. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:633-647 [Conf ] Andrei Voronkov Theorem Proving in Non-Standard Logics Based on the Inverse Method. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:648-662 [Conf ] Konstantin Vershinin , Igor Romanenko One More Logic with Uncertainty and Resolution Principle for it. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:663-667 [Conf ] Li Dafa A Natural Deduction Automated Theorem Proving System. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:668-672 [Conf ] Tobias Nipkow , Lawrence C. Paulson Isabelle-91. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:673-676 [Conf ] Geoff Sutcliffe The Semantically Guided Linear Deduction System. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:677-680 [Conf ] Kurt Ammon The SHUNYATA System. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:681-685 [Conf ] Shang-Ching Chou A Geometry Theorem Prover for Macintoshes. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:686-690 [Conf ] Xin Hua , Hantao Zhang FRI: Failure-Resistant Induction in RRL. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:691-695 [Conf ] Hantao Zhang Herky: High Performance Rewriting in RRL. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:696-700 [Conf ] William M. Farmer , Joshua D. Guttman , F. Javier Thayer IMPS: System Description. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:701-705 [Conf ] Geoffrey D. Alexander , David A. Plaisted Proving Equality Theorems with Hyper-Linking. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:706-710 [Conf ] Jawahar Chirimar , Carl A. Gunter , Myra Van Inwegen Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:711-715 [Conf ] Dave Barker-Plummer , Sidney C. Bailin , Andrew S. Merrill &: Automated Natural Deduction. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:716-720 [Conf ] Tomás E. Uribe , Alan M. Frisch , Michael K. Mitchell An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:721-725 [Conf ] Dave Barker-Plummer , Alex Rothenberg The GAZER Theorem Prover. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:726-730 [Conf ] Ewing L. Lusk , William McCune , John K. Slaney ROO: A Parallel Theorem Prover. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:731-734 [Conf ] Tie-Cheng Wang , Allen Goldberg RVF: An Automated Formal Verification System. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:735-739 [Conf ] Johann Schumann KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract). [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:740-742 [Conf ] K. Blackburn A Report in ICL HOL. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:743-747 [Conf ] Sam Owre , John M. Rushby , Natarajan Shankar PVS: A Prototype Verification System. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:748-752 [Conf ] Wolfgang Reif The KIV System: Systematic Construction of Verified Software. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:753-757 [Conf ] Bernhard Beckert , Stefan Gerberding , Reiner Hähnle , Werner Kernig The Tableau-Based Theorem Prover _{3} T^{A} P for Multi-Valued Logics. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:758-760 [Conf ] Edmund M. Clarke , Xudong Zhao Analytica - A Theorem Prover in Mathematica. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:761-765 [Conf ] Klaus Schneider , Ramayya Kumar , Thomas Kropf The FAUST - Prover. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:766-770 [Conf ] Dan Craigen , Sentot Kromodimoeljo , Irwin Meisels , Bill Pase , Mark Saaltink Eves System Description. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:771-775 [Conf ] Ryuzo Hasegawa , Miyuki Koshimura , Hiroshi Fujita MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:776-780 [Conf ] Ewing L. Lusk , Larry Wos Benchmark Problems in Which Equality Plays the Major Role. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:781-785 [Conf ] David A. Randell , Anthony G. Cohn , Zhan Cui Computing Transivity Tables: A Challenge For Automated Theorem Provers. [Citation Graph (1, 0)][DBLP ] CADE, 1992, pp:786-790 [Conf ]