SHR Tableaux -- A Framework for Automated Model Generation

DOI10.1093/LOGCOM/11.1.107zbMath0986.03017OpenAlexW2127008632MaRDI QIDQ2720403

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

hyperresolutionfinite modelautomated model generationground term rewriting

Mathematics Subject Classification ID

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

Related Items (3)

Representing and building models for decidable subclasses of equational clausal logic ⋮ Some techniques for proving termination of the hyperresolution calculus ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N =

This page was built for publication: SHR Tableaux -- A Framework for Automated Model Generation