Set constraints are the monadic class
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The authors investigate the relationship between set constraints and the monadic class of first-order formulas and show that set constraints are essentially equivalent to the monadic class. From this equivalence, they infer that the satisfiability problem for set constraints is complete for NEXPTIME. More precisely, it is proved that this problem has a lower bound of NTIME(c/sup n/log n/), for some c>0. The relationship between set constraints and the monadic class also gives decidability and complexity results for certain practically useful extensions of set constraints, in particular "negative" projections and subterm equality tests.Keywords
This publication has 14 references indexed in Scilit:
- Theorem proving for hierarchic first-order theoriesPublished by Springer Nature ,2005
- Superposition with simplification as a decision procedure for the monadic class with equalityPublished by Springer Nature ,2005
- Solving systems of set constraintsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Logic programs as types for logic programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A decision procedure for a class of set constraintsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Static type inference in a dynamically typed languagePublished by Association for Computing Machinery (ACM) ,1991
- A finite presentation theorem for approximating logic programsPublished by Association for Computing Machinery (ACM) ,1990
- Flow analysis and optimization of LISP-like structuresPublished by Association for Computing Machinery (ACM) ,1979
- Resolution Strategies as Decision ProceduresJournal of the ACM, 1976
- On the Complexity of Derivation in Propositional CalculusPublished by Springer Nature ,1970