|
Organizers |
Recognising Complexity of True Regular Protothetics Formulas With Partially Ordered Quantifiers
by
Anatoly Beltiukov
Mathematics department, Udmurt State University
Logical formulas that are built with propositional variables, connectives &, \/ , \lnot and quantifiers for all and exists, will be called protothetics formulas. Connectives for all[ ] and exists[ ] will be called partially ordered quantifiers (universal and existentional correspondingly). They are used to construct formulas: for allx[y1, ..., yn]A and existsx[y1, ..., yn]A. The meaning of the statement existsx[y1, ..., yn]A can be informally expressed by the following statement: "Formula A fulfills for some x depending only on values y1, ..., yn".
Prototetics formulas are called to be regular if they do not contain negations placed not immediately before propositional variables and do not contain partially ordered universal quantifiers. All propositional variables are considered to be words of the form vw where v is a symbol, w is a word in the alphabet {0, 1}.
The main result of this work is the following
THEOREM. The problem of recognising true regular protothetics formulas with partially ordered quantifiers is complete for nondeterministic exponential time (with respect to polynomial reducibility).
This result means that partially ordered quantifiers have large expressive power even for so limited theories as protothetics. Note that complexity of the similar problem without partially ordered quantifiers is proved to be in alternating linear time, according to the author's work [1].
Date received: March 1, 1999
Copyright © 1999 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cacs-14.