A decidable fragment of predicate calculus (Q1066880)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A decidable fragment of predicate calculus |
scientific article; zbMATH DE number 3926875
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A decidable fragment of predicate calculus |
scientific article; zbMATH DE number 3926875 |
Statements
A decidable fragment of predicate calculus (English)
0 references
1984
0 references
The authors describe a fragment of the pure predicate calculus which they call direct predicate calculus. It coincides with those formulas that can be proved in the Gentzen sequent calculus without the contraction rule. The direct predicate calculus is shown to be decidable. The procedure first brings a formula into a normal form (in linear time) then applied a characterization of valid sequents in this form.
0 references
direct predicate calculus
0 references
Gentzen sequent calculus without the contraction rule
0 references
