A Proof Procedure Using Connection Graphs

DOI10.1145/321906.321919MaRDI QIDQ4133168zbMATH OpenOpenAlexFDO

Authors Robert Kowalski

Publication date 1975

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/321906.321919

Mathematics Subject Classification ID

Planar graphs; geometric and topological aspects of graph theory (05C10) Algorithms in computer science (68W99)

Cited in

(33)

• Argument graphs and assumption-based argumentation
• Acquiring search-control knowledge via static analysis
• Link inheritance in abstract clause graphs
• Inconsistency check of a set of clauses using Petri net reductions
• Algorithms for Effective Argumentation in Classical Propositional Logic: A Connection Graph Approach
• Paramodulated connection graphs
• Some representational issues in default reasoning
• A perspective on certain polynomial-time solvable classes of satisfiability
• On the termination of clause graph resolution
• A new reduction rule for the connection graph proof procedure
• A new subsumption method in the connection graph proof procedure
• The achievement of knowledge bases by cycle search.
• Speeding up inferences using relevance reasoning: a formalism and algorithms
• Algorithms for generating arguments and counterarguments in propositional logic
• Faster linear unification algorithm
• An Algorithm for Generating Arguments in Classical Predicate Logic
• Compressing propositional refutations
• A logic for default reasoning
• Experiments with resolution-based theorem-proving algorithms
• A new method for knowledge compilation: The achievement by cycle search
• Accelerating tableaux proofs using compact representations
• Reduction rules for resolution-based systems
• MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
• Automated theorem proving methods
• Backchain iteration: Towards a practical inference method that is simple enough to be proved terminating, sound, and complete
• Relational consistency algorithms and their application in finding subgraph and graph isomorphisms
• Formula dissection: A parallel algorithm for constraint satisfaction
• Using rewriting rules for connection graphs to prove theorems
• A comparative study of several proof procedures
• Generating relevant models
• The logic of constraint satisfaction
• Proving with BDDs and control of information
• The linked conjunct method for automatic deduction and related search techniques

This page was built for publication: A Proof Procedure Using Connection Graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4133168)