A-ordered tableaux

DOI10.1093/LOGCOM/6.6.819MaRDI QIDQ2785673zbMATH OpenOpenAlexFDO

Authors Reiner Hähnle, Stefan Klingenbeck

Publication date 14 December 1997

Published in Journal of Logic and Computation (Search for Journal in Brave)

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

zbMATH Keywords

A-orderingsground clause tableaux

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

The main result of the paper is an extension of the resolution proof procedure based on A-orderings of literals (i.e., strict partial orderings respecting substitutions) to the tableau proof procedure. The authors give a simple completeness proof for A-ordered ground clause tableaux and then extend this technique to non-ground non-clausal formulas in the negation normal form by proving completeness of an A-ordered tableau procedure. It is noted that this procedure is not compatible with the connection method.

Recommendations

• Semantic tableaux with ordering restrictions
• Ordered tableaux: extensions and applications
• Ordered semantic hyper tableaux
• A Bottom-Up Approach to Clausal Tableaux
• scientific article; zbMATH DE number 1761419

Cited in

(8)

• scientific article; zbMATH DE number 1614709 (Why is no real title available?)
• scientific article; zbMATH DE number 1090101 (Why is no real title available?)
• scientific article; zbMATH DE number 2079034 (Why is no real title available?)
• Ordered tableaux: extensions and applications
• Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
• A framework for using knowledge in tableau proofs
• scientific article; zbMATH DE number 834570 (Why is no real title available?)
• Semantic tableaux with ordering restrictions

This page was built for publication: A-ordered tableaux

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