Completeness proofs for propositional logic with polynomial-time connectives

Atomic formulas are of the form P(t), where P are monadic predicate variables (which the authors call propositional variables) and t is a term. Composite formulas are constructed by \(\sim\), \&, \(\vee\) and bounded quantfiers \(\forall x\leq t\), \(\exists x\leq t\), as well as \(\forall x\in T\), \(\exists x\in T\) at the end of the paper. When a bounding term is closed, i.e. does not contain individual variables, the corresponding quantifier can be expanded into \& or \(\vee\), which provides completeness and decidability theorem for closed formulas and obvious rules for \(\forall\), \(\exists\). In the presence of free individuum variables, decidability depends of admitted function symbols. The word ``polynomial in the title refers to these functions, not to a decision procedure for derivability.

Recommendations

Cites work

Cited in

(4)

This page was built for publication: Completeness proofs for propositional logic with polynomial-time connectives

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1123883)