Hyperresolution and automated model building
From MaRDI portal
Publication:4880540
DOI10.1093/logcom/6.2.173zbMath0861.68086OpenAlexW2071100103MaRDI QIDQ4880540
Christian G. Fermüller, Alexander Leitsch
Publication date: 9 June 1996
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/logcom/6.2.173
theorem provingmodel buildingresolutionHerbrand modeldecision procedurehyperresolutionatomic representations
Related Items
The model evolution calculus as a first-order DPLL method, Representing and building models for decidable subclasses of equational clausal logic, Some techniques for proving termination of the hyperresolution calculus, Tree tuple languages from the logic programming point of view, Extracting models from clause sets saturated under semantic refinements of the resolution rule., Model building with ordered resolution: Extracting models from saturated clause sets, A calculus combining resolution and enumeration for building finite models, On the complexity of equational problems in CNF, Simplifying and generalizing formulae in tableaux. Pruning the search space and building models, Manipulating Tree Tuple Languages by Transforming Logic Programs1 1Extended abstract; see http://www.logic.at/css/ftp03.pdf for the proofs., A Resolution-based Model Building Algorithm for a Fragment of OCC1N =, Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria, The ground-negative fragment of first-order logic is -complete, On deciding subsumption problems, Decidability Results for Saturation-Based Model Building, Blocking and other enhancements for bottom-up model generation methods, Explicit versus implicit representations of subsets of the Herbrand universe., Efficient model generation through compilation., Working with ARMs: Complexity results on atomic representations of Herbrand models
Uses Software
