Local simplification

DOI10.1006/INCO.1997.2690MaRDI QIDQ1271570zbMATH OpenOpenAlexFDO

Authors K. Appert, Christopher Lynch

Publication date 10 November 1998

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/cb240fec1d4c2d744acc620df6893414f892a5e9

zbMATH Keywords

local simplification inference system

Mathematics Subject Classification ID

Recommendations

• Local simplification
• On the completeness of arbitrary selection strategies for paramodulation
• Selecting the selection
• Theorem-proving with resolution and superposition
• scientific article; zbMATH DE number 1389652

Cites work

• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• AC-superposition with constraints: no AC-unifiers needed
• Associative-commutative deduction with constraints
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Mechanical Theorem-Proving by Model Elimination
• Proving refutational completeness of theorem-proving strategies
• Redundancy criteria for constrained completion
• The Concept of Demodulation in Theorem Proving
• Theorem proving with ordering and equality constrained clauses
• Using forcing to prove completeness of resolution and paramodulation

Cited in

(3)

• scientific article; zbMATH DE number 1389652 (Why is no real title available?)
• Local simplification
• Message reduction in the LOCAL model is a free lunch

This page was built for publication: Local simplification

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