Explicit versus implicit representations of subsets of the Herbrand universe.

DOI10.1016/S0304-3975(02)00583-2zbMath1051.68061MaRDI QIDQ1853582

Reinhard Pichler

Publication date: 21 January 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

ComplexityHerbrand universeImplicit generalizationsNegation elimination

Mathematics Subject Classification ID

General topics in the theory of computing (68Q01)

Related Items

Equational formulas and pattern operations in initial order-sorted algebras ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Explicit representation of terms defined by counter examples
• Equational problems and disunification
• Negation elimination in empty or permutative theories
• Equational formulae with membership constraints
• Working with ARMs: Complexity results on atomic representations of Herbrand models
• On inductive inference of cyclic structures
• Sufficient-completeness, ground-reducibility and their complexity
• An Efficient Unification Algorithm
• An improved lower bound for the elementary theories of trees
• Hyperresolution and automated model building
• The negation elimination from syntactic equational formula is decidable