scientific article; zbMATH DE number 683345

zbMath0810.03007MaRDI QIDQ4312461

Grigori Mints

Publication date: 24 April 1995

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

resolutionintuitionistic predicate logicresolution calculuscut-free Gentzen-type system

Mathematics Subject Classification ID

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

Related Items (5)

Theorem prover for intuitionistic logic based on the inverse method ⋮ A resolution theorem prover for intuitionistic logic ⋮ Optimized encodings of fragments of type theory in first order logic ⋮ The Skolemization of existential quantifiers in intuitionistic logic ⋮ Some pitfalls of LK-to-LJ translations and how to avoid them

This page was built for publication: