Back to Search Start Over

Boolean unification with predicates.

Boolean unification with predicates.

Authors :
EBERHARD, SEBASTIAN
HETZL, STEFAN
WELLER, DANIEL
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