Conferences in DBLP
Peter B. Andrews Connections and Higher-Order Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Leo Bachmair , Nachum Dershowitz Commutation, Transformation, and Termination. [Citation Graph (0, 0)][DBLP ] Conf ] Sara Porat , Nissim Francez Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems. [Citation Graph (0, 0)][DBLP ] Conf ] Ahlem Ben Cherifa , Pierre Lescanne An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations. [Citation Graph (0, 0)][DBLP ] Conf ] Isabelle Gnaedig , Pierre Lescanne Proving Termination of Associative Commutative Rewriting Systems by Rewriting. [Citation Graph (0, 0)][DBLP ] Conf ] Roland Dietrich Relating Resolution and Algebraic Completion for Horn Logic. [Citation Graph (0, 0)][DBLP ] Conf ] David A. Plaisted A Simple Non-Termination Test for the Knuth-Bendix Method. [Citation Graph (0, 0)][DBLP ] Conf ] Rafael Dueire Lins A New Formula for the Execution of Categorial Combinators. [Citation Graph (0, 0)][DBLP ] Conf ] Deepak Kapur , Paliath Narendran , Hantao Zhang Proof by Induction Using Test Sets. [Citation Graph (0, 0)][DBLP ] Conf ] Yoshihito Toyama How to Prove Equivalence of Term Rewriting Systems without Induction. [Citation Graph (0, 0)][DBLP ] Conf ] Hubert Comon Sufficient Completness, Term Rewriting Systems and "Anti-Unification". [Citation Graph (0, 0)][DBLP ] Conf ] Jieh Hsiang , Michaël Rusinowitch A New Method for Establishing Refutational Completeness in Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Gerhard Jäger Some Contributions to the Logical Analysis of Circumscrition. [Citation Graph (0, 0)][DBLP ] Conf ] Martín Abadi , Zohar Manna Modal Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Peter H. Schmitt Computational Aspects of Three-Valued Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Kurt Konolige Resolution and Quantified Epistemic Logics. [Citation Graph (0, 0)][DBLP ] Conf ] Frank M. Brown A Commonsense Theory of Nonmonotonic Reasoning. [Citation Graph (0, 0)][DBLP ] Conf ] Larry Wos , William McCune Negative Paramodulation. [Citation Graph (0, 0)][DBLP ] Conf ] Younghwan Lim The Heuristics and Experimental Results of a New Hyperparamodulation: HL-Resolution. [Citation Graph (0, 0)][DBLP ] Conf ] Tie-Cheng Wang ECR: An Equality Conditional Resolution Proof Procedure. [Citation Graph (0, 0)][DBLP ] Conf ] A. J. J. Dick , Jim Cunningham Using Narrowing to do Isolation in Symbolic Equation Solving - An Experiment in Automated Reasoning. [Citation Graph (0, 0)][DBLP ] Conf ] Tadashi Kanamori , Hiroshi Fujita Formulation of Induction Formulas in Verification of Prolog Programs. [Citation Graph (0, 0)][DBLP ] Conf ] Thomas Käufl Program Verifier "Tatzelwurm": Reasoning about Systems of Linear Inequalities. [Citation Graph (0, 0)][DBLP ] Conf ] Reiner Hähnle , Maritta Heisel , Wolfgang Reif , Werner Stephan An Interactive Verification System Based on Dynamic Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Norbert Eisinger What You Always Wanted to Know About Clause Graph Resolution. [Citation Graph (0, 0)][DBLP ] Conf ] Rasiah Loganantharaj , Robert A. Mueller Parallel Theorem Proving with Connection Graphs. [Citation Graph (0, 0)][DBLP ] Conf ] Neil V. Murray , Erik Rosenthal Theory Links in Semantic Graphs. [Citation Graph (0, 0)][DBLP ] Conf ] David A. Plaisted Abstraction Using Generalization Functions. [Citation Graph (0, 0)][DBLP ] Conf ] Hans-Albert Schneider An Improvement of Deduction Plans: Refutation Plans. [Citation Graph (0, 0)][DBLP ] Conf ] Franz Oppacher , E. Suen Controlling Deduction with Proof Condensation and Heuristics. [Citation Graph (0, 0)][DBLP ] Conf ] Jonathan Traugott Nested Resolution. [Citation Graph (0, 0)][DBLP ] Conf ] Gérard P. Huet Mechanizing Constructive Proofs (Abstract). [Citation Graph (0, 0)][DBLP ] Conf ] Douglas J. Howe Implementing Number Theory: An Experiment with Nuprl. [Citation Graph (0, 0)][DBLP ] Conf ] Cynthia Dwork , Paris C. Kanellakis , Larry J. Stockmeyer Parallel Algorithms for Term Matching. [Citation Graph (2, 0)][DBLP ] Conf ] Erik Tidén Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols. [Citation Graph (0, 0)][DBLP ] Conf ] Alexander Herold Combination of Unification Algorithms. [Citation Graph (0, 0)][DBLP ] Conf ] Wolfram Büttner Unification in the Data Structure Sets. [Citation Graph (1, 0)][DBLP ] Conf ] Deepak Kapur , Paliath Narendran NP-Completeness of the Set Unification and Matching Problems. [Citation Graph (2, 0)][DBLP ] Conf ] Jalel Mzali Matching with Distributivity. [Citation Graph (0, 0)][DBLP ] Conf ] Ursula Martin , Tobias Nipkow Unification in Boolean Rings. [Citation Graph (0, 0)][DBLP ] Conf ] Hans-Jürgen Bürckert Some Relationships between Unification, restricted Unification, and Matching. [Citation Graph (0, 0)][DBLP ] Conf ] Christoph Walther A Classification of Many-Sorted Unification Problems. [Citation Graph (0, 0)][DBLP ] Conf ] Manfred Schmidt-Schauß Unification in Many-Sorted Eqational Theories. [Citation Graph (0, 0)][DBLP ] Conf ] Hans Kleine Büning , Theodor Lettmann Classes of First Order Formulas Under Various Satisfiability Definitions. [Citation Graph (0, 0)][DBLP ] Conf ] Volker Weispfenning Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs. [Citation Graph (0, 0)][DBLP ] Conf ] Mark E. Stickel A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. [Citation Graph (0, 0)][DBLP ] Conf ] Ralph Butler , Ewing L. Lusk , William McCune , Ross A. Overbeek Paths to High-Performance Automated Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] F. Keith Hanna , Neil Daeche Purely Functional Implementation of a Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Philip T. Cox , Tomasz Pietrzykowski Causes for Events: Their Computation and Applications. [Citation Graph (0, 0)][DBLP ] Conf ] Zohar Manna , Richard J. Waldinger How to Clear a Block: Plan Formation in Situational Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Jonathan Traugott Deductive Synthesis of Sorting Programs. [Citation Graph (0, 0)][DBLP ] Conf ] Peter B. Andrews , Frank Pfenning , Sunil Issar , C. P. Klapper The TPS Theorem Proving System. [Citation Graph (0, 0)][DBLP ] Conf ] Jürgen Avenhaus , Benjamin Benninghofen , Rüdiger Göbel , Klaus Madlener TRSPEC: A Term Rewriting Based System for Algebraic Specifications. [Citation Graph (0, 0)][DBLP ] Conf ] M. Bayerl Highly Parallel Inference Machine. [Citation Graph (0, 0)][DBLP ] Conf ] Christoph Beierle , Walter G. Olthoff , Angi Voß Automatic Theorem Proving in the ISDV System. [Citation Graph (0, 0)][DBLP ] Conf ] Susanne Biundo , B. Hummel , Dieter Hutter , Christoph Walther The Karlsruhe Induction Theorem Proving System. [Citation Graph (0, 0)][DBLP ] Conf ] Robert S. Boyer , J. Strother Moore Overview of a Theorem-Prover for A Computational Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Shang-Ching Chou GEO-Prover - A Geometry Theorem Prover Developed at UT. [Citation Graph (0, 0)][DBLP ] Conf ] Norbert Eisinger , Hans Jürgen Ohlbach The Markgraf Karl Refutation Procedure (MKRP). [Citation Graph (0, 0)][DBLP ] Conf ] Jacek Gibert The J-Machine: Functional Programming with Combinators. [Citation Graph (0, 0)][DBLP ] Conf ] Steven Greenbaum , David A. Plaisted The Illinois Prover: A General Purpose Resolution Theorem Prover. [Citation Graph (0, 0)][DBLP ] Conf ] Gérard P. Huet Theorem Proving Systems of the Formel Project. [Citation Graph (0, 0)][DBLP ] Conf ] Heinrich Hußmann The Passau RAP System: Prototyping Algebraic Specifications Using Conditional Narrowing. [Citation Graph (0, 0)][DBLP ] Conf ] Deepak Kapur , G. Sivakumar , Hantao Zhang RRL: A Rewrite Rule Laboratory. [Citation Graph (0, 0)][DBLP ] Conf ] B. Kutzler , Sabine Stifter A Geometry Theorem Prover Based on Buchberger's Algorithm. [Citation Graph (0, 0)][DBLP ] Conf ] Pierre Lescanne REVE a Rewrite Rule Laboratory. [Citation Graph (0, 0)][DBLP ] Conf ] Ewing L. Lusk , William McCune , Ross A. Overbeek ITP at Argonne National Laboratory. [Citation Graph (0, 0)][DBLP ] Conf ] Charles G. Morgan AUTOLOGIC at University of Victoria. [Citation Graph (0, 0)][DBLP ] Conf ] Francis Jeffry Pelletier THINKER. [Citation Graph (0, 0)][DBLP ] Conf ] Mark E. Stickel The KLAUS Automated Deduction System. [Citation Graph (0, 0)][DBLP ] Conf ] Paul B. Thistlewaite , Michael A. McRobbie , Robert K. Meyer The KRIPKE Automated Theorem Proving System. [Citation Graph (0, 0)][DBLP ] Conf ] Tie-Cheng Wang SHD-Prover at University of Texas at Austin. [Citation Graph (0, 0)][DBLP ] Conf ] 