Working with ARMs: Complexity results on atomic representations of Herbrand models

DOI10.1006/inco.2000.2915zbMath1007.03009OpenAlexW1964789714WikidataQ59259728 ScholiaQ59259728MaRDI QIDQ1854418

Georg Gottlob, Reinhard Pichler

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.2000.2915

zbMATH Keywords

computational complexityatomic representationdecision problemsHerbrand modelcoNP-complete problems

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ On deciding subsumption problems ⋮ Constructing infinite models represented by tree automata ⋮ Automated Model Building: From Finite to Infinite Models ⋮ Explicit versus implicit representations of subsets of the Herbrand universe.

Cites Work

• A non-ground realization of the stable and well-founded semantics
• Explicit representation of terms defined by counter examples
• Equational problems and disunification
• Linear unification
• Sufficient-completeness, ground-reducibility and their complexity
• Using resolution for deciding solvable classes and building finite models
• An improved lower bound for the elementary theories of trees
• Hyperresolution and automated model building
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item