A decidable fragment of predicate calculus

DOI10.1016/0304-3975(84)90047-1zbMath0579.03007OpenAlexW2057599103MaRDI QIDQ1066880

Jussi Ketonen, Richard W. Weyhrauch

Publication date: 1984

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(84)90047-1

zbMATH Keywords

direct predicate calculusGentzen sequent calculus without the contraction rule

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Semantics of weakening and contraction, Predicate logics without the structure rules, Limited reasoning in first-order knowledge bases, Remarks on a survey article on many valued logic by A. Urquhart, European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium '88), Padova, 1988, Limited reasoning in first-order knowledge bases with full introspection, Causal dependencies in multiplicative linear logic with MIX, On contraction and the modal fragment, Automatic theorem proving. II, Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials, A decision procedure revisited: Notes on direct logic, linear logic and its implementation, Decision problems for propositional linear logic, Towards Hilbert's 24th Problem: Combinatorial Proof Invariants, On the Methodology of Paraconsistent Logic, Connection methods in linear logic and proof nets construction

Cites Work

• Toward Mechanical Mathematics
• Theorem Proving via General Matings
• Unnamed Item
• Unnamed Item