Pruning the search space and extracting more models in tableaux

DOI10.1093/JIGPAL/7.2.217MaRDI QIDQ4237680zbMATH OpenOpenAlexFDO

Authors Nicolas Peltier

Publication date 6 December 2000

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/7.2.217

zbMATH Keywords

decidable classesextension of tableauxHintikka setsmodel building

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
• A more efficient tableaux procedure for simultaneous search for refutations and finite models
• A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
• SHR tableaux -- a framework for automated model generation

Cited in

(9)

• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• The model evolution calculus as a first-order DPLL method
• SHR tableaux -- a framework for automated model generation
• Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
• scientific article; zbMATH DE number 69315 (Why is no real title available?)
• scientific article; zbMATH DE number 1323296 (Why is no real title available?)
• scientific article; zbMATH DE number 1552525 (Why is no real title available?)
• Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
• A more efficient tableaux procedure for simultaneous search for refutations and finite models

This page was built for publication: Pruning the search space and extracting more models in tableaux

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