A decidable fragment of predicate calculus
From MaRDI portal
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.
Recommendations
- A decision procedure revisited: Notes on direct logic, linear logic and its implementation
- The complexity of decision procedures in relevance logic II
- scientific article; zbMATH DE number 2187724
- On contraction and the modal fragment
- Eigenvariables, bracketing and the decidability of positive minimal predicate logic
Cites work
Cited in
(27)- Predicate logics without the structure rules
- Remarks on a survey article on many valued logic by A. Urquhart
- A general method of axiomatizing fragments
- A decision procedure revisited: Notes on direct logic, linear logic and its implementation
- Decision problems for propositional linear logic
- Semantics of weakening and contraction
- Limited reasoning in first-order knowledge bases
- Connection methods in linear logic and proof nets construction
- Limited reasoning in first-order knowledge bases with full introspection
- scientific article; zbMATH DE number 1696781 (Why is no real title available?)
- scientific article; zbMATH DE number 4202241 (Why is no real title available?)
- European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium '88), Padova, 1988
- On contraction and the modal fragment
- Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials
- Decidability properties for fragments of CHR
- Automatic theorem proving. II
- scientific article; zbMATH DE number 1303435 (Why is no real title available?)
- Monadic decomposition
- FUNCTIONAL PEARL Functional satisfaction
- Predicative Fragments of Frege Arithmetic
- Causal dependencies in multiplicative linear logic with MIX
- Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
- Decidable fragments of field theories
- On the methodology of paraconsistent logic
- scientific article; zbMATH DE number 2187724 (Why is no real title available?)
- Liss — The logic inference search system
- Tractable fragments of Presburger arithmetic
This page was built for publication: A decidable fragment of predicate calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1066880)
