Explicit versus implicit representations of subsets of the Herbrand universe.

DOI10.1016/S0304-3975(02)00583-2MaRDI QIDQ1853582zbMATH OpenFDO

Authors Reinhard Pichler

Publication date 21 January 2003

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

Full work available at URL https://doi.org/10.1016/S0304-3975(02)00583-2

zbMATH Keywords

ComplexityHerbrand universeImplicit generalizationsNegation elimination

Mathematics Subject Classification ID

General topics in the theory of computing (68Q01)

Recommendations

• scientific article; zbMATH DE number 1615238
• Negation elimination in empty or permutative theories
• Explicit representation of terms defined by counter examples
• scientific article; zbMATH DE number 4011966
• scientific article; zbMATH DE number 1670857

Cites work

• An Efficient Unification Algorithm
• An improved lower bound for the elementary theories of trees
• Equational formulae with membership constraints
• Equational problems and disunification
• Explicit representation of terms defined by counter examples
• scientific article; zbMATH DE number 1615238 (Why is no real title available?)
• scientific article; zbMATH DE number 1670857 (Why is no real title available?)
• scientific article; zbMATH DE number 4053011 (Why is no real title available?)
• scientific article; zbMATH DE number 176121 (Why is no real title available?)
• scientific article; zbMATH DE number 1341610 (Why is no real title available?)
• scientific article; zbMATH DE number 549974 (Why is no real title available?)
• Hyperresolution and automated model building
• Negation elimination in empty or permutative theories
• On inductive inference of cyclic structures
• Sufficient-completeness, ground-reducibility and their complexity
• The negation elimination from syntactic equational formula is decidable
• Working with ARMs: Complexity results on atomic representations of Herbrand models

Cited in

(5)

• Explicit representation of terms defined by counter examples
• Equational formulas and pattern operations in initial order-sorted algebras
• scientific article; zbMATH DE number 845928 (Why is no real title available?)
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Equational formulas and pattern operations in initial order-sorted algebras

This page was built for publication: Explicit versus implicit representations of subsets of the Herbrand universe.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1853582)