A Proof Procedure Using Connection Graphs
From MaRDI portal
Publication:4133168
DOI10.1145/321906.321919zbMath0357.68097OpenAlexW1970045008MaRDI QIDQ4133168
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
Planar graphs; geometric and topological aspects of graph theory (05C10) Algorithms in computer science (68W99)
Related Items
Accelerating tableaux proofs using compact representations, On the termination of clause graph resolution, Link inheritance in abstract clause graphs, Inconsistency check of a set of clauses using Petri net reductions, A new reduction rule for the connection graph proof procedure, MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics, Speeding up inferences using relevance reasoning: a formalism and algorithms, Using rewriting rules for connection graphs to prove theorems, A logic for default reasoning, Relational consistency algorithms and their application in finding subgraph and graph isomorphisms, Experiments with resolution-based theorem-proving algorithms, Algorithms for generating arguments and counterarguments in propositional logic, Formula dissection: A parallel algorithm for constraint satisfaction, Reduction rules for resolution-based systems, A new method for knowledge compilation: The achievement by cycle search, Acquiring search-control knowledge via static analysis, A new subsumption method in the connection graph proof procedure, The logic of constraint satisfaction, Compressing Propositional Refutations, Algorithms for Effective Argumentation in Classical Propositional Logic: A Connection Graph Approach, Proving with BDDs and control of information, Paramodulated connection graphs, An Algorithm for Generating Arguments in Classical Predicate Logic, A comparative study of several proof procedures, The linked conjunct method for automatic deduction and related search techniques, Some representational issues in default reasoning, Automated theorem proving methods, The achievement of knowledge bases by cycle search., Faster linear unification algorithm, Backchain iteration: Towards a practical inference method that is simple enough to be proved terminating, sound, and complete, A perspective on certain polynomial-time solvable classes of satisfiability, Generating relevant models, Argument graphs and assumption-based argumentation
