Restart tableaux with selection function

DOI10.1007/3-540-63385-5_45MaRDI QIDQ4364517zbMATH OpenFDO

Authors Christian Pape, Reiner Hähnle

Publication date 17 November 1997

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://publikationen.bibliothek.kit.edu/74197/2221

zbMATH Keywords

model eliminationproof confluence propertyproof searchrestart clausesselection functiontableau calculi

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

The paper presents two variants of tableau calculi which generalize some known tableau calculi based on the idea of selection function and restart clauses. Using the selection function (which selects some literals from clauses) one is able to order the process of building a tableau proof and to restrict the search space. The soundness and completeness of these calculi for a ground level are proved. Lifting to first-order logic can be done as usual. The proof confluence property for tableaux with selection function is stated. For the entire collection see [Zbl 0870.00023].

Recommendations

• Ordered tableaux: extensions and applications
• scientific article; zbMATH DE number 1552524
• Tableaux and related methods
• Hyper tableaux

Cited in

(2)

• scientific article; zbMATH DE number 1552524 (Why is no real title available?)
• Ordered tableaux: extensions and applications

This page was built for publication: Restart tableaux with selection function

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