Pruning the search space and extracting more models in tableaux

DOI10.1093/jigpal/7.2.217zbMath0949.03013OpenAlexW2041023020MaRDI QIDQ4237680

Nicolas Peltier

Publication date: 6 December 2000

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

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

zbMATH Keywords

model buildingdecidable classesextension of tableauxHintikka sets

Mathematics Subject Classification ID

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

Related Items (3)

Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ The model evolution calculus as a first-order DPLL method ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule.

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