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

DOI10.1006/inco.2000.2915zbMath1007.03009WikidataQ59259728 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 complexity; atomic representation; decision problems; Herbrand model; coNP-complete problems

Mathematics Subject Classification ID

03B25: Decidability of theories and sets of sentences

03B35: Mechanization of proofs and logical operations

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

Related Items

A Resolution-based Model Building Algorithm for a Fragment of OCC1N =, Automated Model Building: From Finite to Infinite Models, Constructing infinite models represented by tree automata, On deciding subsumption problems, 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