Back to Search
Start Over
Boolean unification with predicates.
Boolean unification with predicates.
- Source :
- Journal of Logic & Computation; Feb2017, Vol. 27 Issue 1, p109-128, 20p
- Publication Year :
- 2017
-
Abstract
- In this article, we deal with the following problem which we call Boolean unification with predicates: For a given formula F[X ] in first-order logic with equality containing an n-ary predicate variable X, is there a quantifier-free formula G[x<subscript>1</subscript>,…,x<subscript>n</subscript>] such that the formula F[G] is valid in first-order logic with equality? We obtain the following results. Boolean unification with predicates for quantifier-free F is π<superscript>P</superscript><subscript>2</subscript>-complete. In addition, there exists an EXPTIME algorithm which for an input formula F[X ], given as above, constructs a formula G such that F[G] being valid in first-order logic with equality, if such a formula exists. For F of the form ∀¯yF'[X,¯y] with F' quantifier-free, we prove that Boolean unification with predicates is already undecidable. The same holds for F of the form ∃¯yF'[X,¯y] for F' quantifier-free. Instances of Boolean unification with predicates naturally occur in the context of automated theorem proving. Our results are relevant for cut-introduction and the automated search for induction invariants. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 0955792X
- Volume :
- 27
- Issue :
- 1
- Database :
- Complementary Index
- Journal :
- Journal of Logic & Computation
- Publication Type :
- Academic Journal
- Accession number :
- 121020067
- Full Text :
- https://doi.org/10.1093/logcom/exv059