scientific article; zbMATH DE number 683345

MaRDI QIDQ4312461zbMATH OpenFDO

Authors G. E. Mints

Publication date 24 April 1995

zbMATH Keywords

cut-free Gentzen-type systemintuitionistic predicate logicresolutionresolution calculus

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Recommendations

• A resolution theorem prover for intuitionistic logic
• scientific article; zbMATH DE number 517062
• Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic
• Publication:3485886
• Resolution calculi for modal logics
• Resolution-based methods for modal logics
• scientific article; zbMATH DE number 4027425
• scientific article; zbMATH DE number 1324434
• scientific article; zbMATH DE number 4055570
• Extending resolution to resolution logics

Cited in

(19)

• Labelled resolution for classical and non-classical logics
• Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic
• Theorem prover for intuitionistic logic based on the inverse method
• The Skolemization of existential quantifiers in intuitionistic logic
• Extending resolution to resolution logics
• scientific article; zbMATH DE number 4160687 (Why is no real title available?)
• scientific article; zbMATH DE number 3941499 (Why is no real title available?)
• scientific article; zbMATH DE number 4027425 (Why is no real title available?)
• scientific article; zbMATH DE number 15881 (Why is no real title available?)
• scientific article; zbMATH DE number 77919 (Why is no real title available?)
• scientific article; zbMATH DE number 1303346 (Why is no real title available?)
• scientific article; zbMATH DE number 510785 (Why is no real title available?)
• scientific article; zbMATH DE number 517062 (Why is no real title available?)
• scientific article; zbMATH DE number 1479612 (Why is no real title available?)
• A resolution theorem prover for intuitionistic logic
• Proof-terms for classical and intuitionistic resolution
• Optimized encodings of fragments of type theory in first order logic
• Completeness of Resolution for Definite Answers
• Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them

This page was built for publication:

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