Using rewriting rules for connection graphs to prove theorems
Artificial IntelligencePublished 1 August 1979
C. L. Chang, J.R. Slagle
Citations38
SJR quartileQ1
SJR score1.84
SNIP3.30
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A method to obtain rewriting rules from the graph is described, and it is shown that these rewriting rules can be used to generate a refutation plan that may correspond to a large number of linear resolution refutations.
Abstract
Essentially, a connection graph is merely a data structure for a set of clauses indicating possible refutations. The graph itself is not an inference system. To use the graph, one has to introduce operations on the graph. In this paper, we shall describe a method to obtain rewriting rules from the graph, and then to show that these rewriting rules can be used to generate a refutation plan that may correspond to a large number of linear resolution refutations. Using this method, many redundant resolution steps can be avoided.
Keywords
Computer Science
Journal of the ACMA Machine-Oriented Logic Based on the Resolution Principle
3,885 Citations1965John A. Robinson
The paper concludes with a discussion of several principles which are applicable to the design of efficient proof-procedures employing resolution as the basle logical process.
Elsevier eBooksSymbolic Logic and Mechanical Theorem Proving
1,472 Citations1973
This book contains an introduction to symbolic logic and a thorough discussion of mechanical theorem proving its applications and how it can be applied to various areas such as question answering, problem solving, program analysis, and program synthesis.
ACM Transactions on Programming Languages and SystemsAn Efficient Unification Algorithm
772 Citations1982Alberto Martelli, Ugo Montanari
A new unification algorithm, characterized by having the acyclicity test efficiently embedded into it, is derived from the nondeterministic one, and a PASCAL implementation is given.
Journal of the ACMA Proof Procedure Using Connection Graphs
254 Citations1975Robert Kowalski
A new theorem-proving system designed to remedy deficiencies of resolution systems is presented, beginning as a supplement to SL-resolution in the form of classificatmn trees and incorporating an analogue of the Waltz algorithm for picture Interpretation.
Prolog - the language and its implementation compared with Lisp
242 Citations1977David H. Warren, Luís M.C. Pereira +1 more
It is argued that pattern matching is a better method for expressing operations on structured data than conventional selectors and constructors - both for the user and for the implementor.
Lecture notes in computer sciencePattern Recognition and Artificial Intelligence
159 Citations2022Mounîm A. El‐Yacoubi, Éric Granger +3 more
Artificial IntelligenceRefutation graphs
97 Citations1976Robert E. Shostak
A graph-theoretic characterization of truth-functional consistency is introduced, providing a clear perspective on some resolution-based for deciding formulas in propositional and first-order logic.
IEEE Transactions on ComputersA Search Technique for Clause Interconnectivity Graphs
84 Citations1976Sickel
A new representation and technique for proving theorems automatically that is both computationally more effective than resolution and permits a clear and concise formal description is presented.
IEEE Transactions on ComputersRefutations by Matings
70 Citations1976Andrews
The existence of many refutations with the same mating leads to wasteful redundancy in the search for a refutation, so it is natural to focus on the essential problem of finding appropriate matings.
DEDUCE 2: Further Investigations of Deduction in Relational Data Bases
70 Citations1978C. L. Chang
A new syntax of DEDUCE is given for uniformly handling queries having existential, universal or numerical quantifiers and an optimization problem about access methods for efficient deductions in a relational data base will be discussed.
A production system for automatic deduction
22 Citations1977Nils J. Nilsson
A new predicate calculus deduction system based on production rules that can handle the full range of predicate calculus expressions including those with quantified variables, disjunctions and negations is proposed.
Information SciencesTheorem proving with variable-constrained resolution
16 Citations1972C. L. Chang
Using V-resolution, it is guaranteed that the empty clause @?
ACM SIGART BulletinPlanning techniques for rule selection in deductive question-answering
9 Citations1977Philip Klahr
Deductive planning techniques are described for rule selection in question-answering systems and the applicability and generality of these techniques for use in other rule-based systems is discussed.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)Formal grammars as models of logic derivations
7 Citations1977Sharon Sickel
The method reported here is unique in being able to characterize all proofs of some theorems, representing even an infinite set of proofs with a finite formula.