Model Elimination and Connection Tableau Procedures

No abstract is available for this paper.

• Publication year

  2001

• Venue

  Handbook of Automated Reasoning

• Publication date

  Unknown publication date

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1016/b978-044450813-3/50030-8
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Automated Theorem Proving

  2014cited by this paper
• First-Order Logic

  2008cited by this paper
• Proof search without backtracking for free variable tableaux

  2002cited by this paper
• Tableaux and Related Methods

  2001cited by this paper
• Combining Superposition, Sorts and Splitting

  2001cited by this paper
• Resolution Theorem Proving

  2001cited by this paper
• A Confluent Connection Calculus

  1999cited by this paper
• Hyper Tableau - The Next Generation

  1998cited by this paper
• Using Matings for Pruning Connection Tableaux

  1998cited by this paper
• Elimination of Equality via Transformation with Ordering Constraints

  1998cited by this paper
• First-order logic and automated theorem proving (2nd ed.)

  1996cited by this paper
• The Disconnection Method - A Confluent Integration of Unification in the Analytic Framework

  1996cited by this paper
• Optimizing Proof Search in Model Elimination

  1996cited by this paper
• Specifications of Inference Rules and Their Automatic Translation

  1995cited by this paper
• SETHEO V3.2: Recent Developments - System Abstract

  1994cited by this paper
• PROTEIN: A PROver with a Theory Extension INterface

  1994cited by this paper
• Semantic Tableaux with Ordering Restrictions

  1994cited by this paper
• Refinements and Extensions of Model Elimination

  1993cited by this paper
• Two problems-two solutions: one system-ECLIPSE

  1993cited by this paper
• Complexity of Resolution Proofs and Function Introduction

  1992cited by this paper
• Caching and Lemmaizing in Model Elimination Theorem Provers

  1992cited by this paper
• An Improved Method for Adding Equality to Free Variable Semantic Tableaux

  1992cited by this paper
• PARTHEO: A High-Performance Parallel Theorem Prover

  1990cited by this paper
• A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog

  1990cited by this paper
• First-Order Logic and Automated Theorem Proving

  1990cited by this paper
• Minimizing the Number of Clauses by Renaming

  1990cited by this paper
• METEORs: High Performance Theorem Provers Using Model Elimination

  1990cited by this paper
• KCM: A Knowledge Crunching Machine

  1989cited by this paper
• Equational Problems and Disunification

  1989cited by this paper
• Automated theorem proving (second revised edition) by Wolfgang Bibel, Vieweg 1987

  1988cited by this paper
• A New Abstract Prolog Instruction Set

  1987cited by this paper
• Compilers: Principles, Techniques, and Tools

  1986cited by this paper
• A Structure-Preserving Clause Form Translation

  1986cited by this paper
• Iterative-Deepening-A*: An Optimal Admissible Tree Search

  1985cited by this paper
• Hardware Design and Implementation of the Personal Sequential Inference Machine (PSI)

  1984cited by this paper
• An Implementation of a Theorem Prover Based on the Connection Method

  1984cited by this paper
• A Rehabilitation of Robinson's Unification Algorithm

  1983cited by this paper
• Automation of Reasoning

  1983cited by this paper
• Theorem Proving via General Matings

  1981cited by this paper
• Automated theorem proving: a logical basis

  1978cited by this paper
• Principles of Compiler Design (Addison-Wesley series in computer science and information processing)

  1977cited by this paper
• Principles of Compiler Design

  1977cited by this paper
• Refutation Graphs

  1976cited by this paper
• Proving Theorems with the Modification Method

  1975cited by this paper
• A Unifying View of Some Linear Herbrand Procedures

  1972cited by this paper
• Linear Resolution with Selection Function

  1971cited by this paper
• A Simplified Format for the Model Elimination Theorem-Proving Procedure

  1969cited by this paper
• Mechanical Theorem-Proving by Model Elimination

  1968cited by this paper
• Untersuchungen über das logische Schließen. I

  1935cited by this paper

• Constraint Learning for Non-confluent Proof Search

  2026influential citation
• Explaining the undecidability of first-order logic

  2025cites this paper
• Interpolation with Automated First-Order Reasoning

  2025cites this paper
• Range-Restricted Interpolation through Clausal Tableaux

  2023cites this paper
• 20 Years of leanCoP - An Overview of the Provers

  2023influential citation
• A Syntax for Connection Proofs

  2023influential citation
• CD Tools - Condensed Detachment and Structure Generating Theorem Proving (System Description)

  2022influential citation
• Compressed Combinatory Proof Structures and Blending Goal-with Axiom-Driven Reasoning: Perspectives for First-Order ATP with Condensed Detachment and Clausal Tableaux

  2022cites this paper
• Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving

  2022influential citation
• Lazy Paramodulation in Practice

  2022influential citation
• Set of Support, Demodulation, Paramodulation: A Historical Perspective

  2022cites this paper
• A Curiously Effective Backtracking Strategy for Connection Tableaux

  2021cites this paper
• The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics

  2021cites this paper
• Machine Learning Guidance for Connection Tableaux

  2020cites this paper
• Automated Theorem Proving, Fast and Slow

  2020cites this paper
• From Schütte’s Formal Systems to Modern Automated Deduction

  2020cites this paper
• Craig Interpolation with Clausal First-Order Tableaux

  2020cites this paper
• Prolog Technology Reinforcement Learning Prover

  2020cites this paper
• Certification of Nonclausal Connection Tableaux Proofs

  2019cites this paper
• Machine Learning Guidance and Proof Certification for Connection Tableaux

  2018cites this paper
• The Pocket Reasoner -- Automatic Reasoning on Small Devices

  2018cites this paper
• A Tableaux Calculus for Reducing Proof Size

  2018cites this paper
• Parallel Theorem Proving

  2018cites this paper
• Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux

  2018cites this paper
• Proof Search Optimizations for Non-Clausal Connection Calculi

  2018cites this paper
• Automated Reasoning with Analytic Tableaux and Related Methods

  2017cites this paper
• Non-clausal Connection Calculi for Non-classical Logics

  2017cites this paper
• Advances in Connection-Based Automated Theorem Proving

  2017cites this paper
• Mathematical Text Processing in EA-style : a Sequent Approach

  2016cites this paper
• Mathematical Text Processing in EA-style: a Sequent Aspect

  2016cites this paper
• Efficient Low-Level Connection Tableaux

  2015cites this paper
• Semantically-Guided Goal-Sensitive Reasoning: Model Representation

  2015cites this paper
• Proof Generation for Saturating First-Order Theorem Provers

  2014cites this paper
• Certified Connection Tableaux Proofs for HOL Light and TPTP

  2014cites this paper
• Exploring Automated Reasoning in First-Order Logic: Tools, Techniques and Application Areas

  2013cites this paper
• External sources of axioms in lean theorem proving

  2012cites this paper
• Tableau-Based Reasoning for Decidable Fragments of First-Order Logic

  2012cites this paper
• Using the TPTP Language for Representing Derivations in Tableau andConnection Calculi

  2012influential citation
• A Non-clausal Connection Calculus

  2011cites this paper
• From Proof Trees to Justificatory Answering

  2011cites this paper
• Proceedings of the CADE-23 ATP System Competition CASC-23

  2011cites this paper
• Bottom-up Construction of Semantic Tableaux

  2010cites this paper
• Specifying and Verifying Organizational Security Properties in First-Order Logic

  2010cites this paper
• Extracting Case-based Answers from Closed Proof-trees

  2010cites this paper
• Restricting backtracking in connection calculi

  2010influential citation
• SOLAR: An automated deduction system for consequence finding

  2010cites this paper
• The CADE-22 ATP System Competition (CASC-22)

  2009cites this paper
• Evolving model evolution

  2009cites this paper
• Knowledge Representation and Classical Logic

  2008cites this paper
• Encoding First Order Proofs in SMT

  2008cites this paper
• leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)

  2008influential citation
• randoCoP: Randomizing the Proof Search Order in the Connection Calculus

  2008cites this paper
• Introduction to Logic and Automated Theorem Proving

  2007cites this paper
• A Sound Framework for δ-Rule Variants in Free-Variable Semantic Tableaux

  2007cites this paper
• A Bottom-Up Approach to Clausal Tableaux

  2007cites this paper
• Encoding First Order Proofs in SAT

  2007cites this paper
• Lemma Learning in the Model Evolution Calculus

  2006cites this paper
• SAD as a mathematical assistant - how should we go from here to there?

  2006cites this paper
• Connection Tableaux with Lazy Paramodulation

  2006cites this paper
• Access Control Policy Analysis Using Free Variable Tableaux

  2006cites this paper
• Implementing the Model Evolution Calculus

  2006cites this paper
• The SAD System: Deductive Assistance in an Intelligent Linguistic Environment

  2006cites this paper
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies

  2005influential citation
• Model Representation via Contexts and Implicit Generalizations

  2005cites this paper
• Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic

  2005cites this paper
• Theorem Proving and Proof Verification in the System SAD

  2004cites this paper
• Uniform variable splitting

  2004cites this paper
• Discovering attacks on security protocols by refuting incorrect inductive conjectures

  2004cites this paper
• Computer-Oriented Calculi of Sequent Trees

  2004cites this paper
• The CADE-19 ATP System Competition (CASC-19)

  2003cites this paper
• Hierarchical contextual reasoning

  2003cites this paper
• Automated Reasoning: Past Story and New Trends

  2003cites this paper
• First-order logic Davis-Putnam-Logemann-Loveland procedure

  2003influential citation
• The CADE-18 ATP System Competition (CASC-18)

  2002cites this paper
• Proof search without backtracking for free variable tableaux

  2002cites this paper
• Encoding Two-Valued Nonclassical Logics in Classical Logic

  2001cites this paper
• Connections in Nonclassical Logics

  2001cites this paper
• The Inverse Method

  2001cites this paper
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae

  2001cites this paper
• Incremental Closure of Free Variable Tableaux

  2001cites this paper
• Tableaux and Related Methods

  2001cites this paper
• Certified Connection Tableaux Proofs for HOL Light and TPTP

  year unknowncites this paper
• Handbook of Knowledge Representation Edited Knowledge Representation and Classical Logic

  year unknowncites this paper