An improved lower bound for the elementary theories of trees

DOI10.1007/3-540-61511-3_91zbMath1415.03039OpenAlexW2096975981MaRDI QIDQ4647523

Sergei Vorobyov

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_91

zbMATH Keywords

binary relationlogic programmingfirst-order theory of trees

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Logic programming (68N17) Basic properties of first-order languages and structures (03C07)

Related Items

The first order theory of primal grammars is decidable, Extracting models from clause sets saturated under semantic refinements of the resolution rule., Unnamed Item, A Full First-Order Constraint Solver for Decomposable Theories, Explicit versus implicit representations of subsets of the Herbrand universe., Ordering constraints over feature trees expressed in second-order monadic logic., Working with ARMs: Complexity results on atomic representations of Herbrand models

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A complete and recursive feature theory
• A uniform method for proving lower bounds on the computational complexity of logical theories
• Equational problems and disunification
• Classical recursion theory. The theory of functions and sets of natural numbers
• The computational complexity of logical theories
• How to win a game with features
• A feature constraint system for logic programming with entailment
• A complete axiomatization of a theory with feature and arity constraints
• Theory of Formal Systems. (AM-47)
• Negation in logic programming
• Feature-constraint logics for unification grammars
• Separating Nondeterministic Time Complexity Classes
• Records for logic programming