SHR tableaux -- a framework for automated model generation

DOI10.1093/LOGCOM/11.1.107MaRDI QIDQ2720403zbMATH OpenOpenAlexFDO

Authors Thomas M. Rudlof

Publication date 6 June 2002

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

Full work available at URL https://doi.org/10.1093/logcom/11.1.107

zbMATH Keywords

automated model generationfinite modelground term rewritinghyperresolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Model theory of finite structures (03C13) Grammars and rewriting systems (68Q42)

Recommendations

• Positive unit hyperresolution tableaux and their application to minimal model generation
• 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
• Hyperresolution and automated model building
• Pruning the search space and extracting more models in tableaux

Cited in

(7)

• Efficient model generation through compilation.
• Pruning the search space and extracting more models in tableaux
• scientific article; zbMATH DE number 1088032 (Why is no real title available?)
• A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
• A more efficient tableaux procedure for simultaneous search for refutations and finite models
• Representing and building models for decidable subclasses of equational clausal logic
• Some techniques for proving termination of the hyperresolution calculus

This page was built for publication: SHR tableaux -- a framework for automated model generation

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