scientific article; zbMATH DE number 4170865

MaRDI QIDQ3496309zbMATH OpenFDO

Authors A. A. Voronkov

Publication date 1990

zbMATH Keywords

Gentzen-like calculusMaslov's inverse methodproof search method for first order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Decidability of the class E by Maslov's inverse method
• scientific article; zbMATH DE number 1348471
• Publication:4729755
• scientific article; zbMATH DE number 3992945
• scientific article; zbMATH DE number 2079834

Cited in

(18)

• Evidence algorithm and inference search in first-order logics
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Disproving using the inverse method by iterative refinement of finite approximations
• Decidability of the class E by Maslov's inverse method
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• scientific article; zbMATH DE number 3985190 (Why is no real title available?)
• scientific article; zbMATH DE number 1348471 (Why is no real title available?)
• First-order theorem proving: foreword
• scientific article; zbMATH DE number 2079834 (Why is no real title available?)
• scientific article; zbMATH DE number 1761887 (Why is no real title available?)
• First-order Answer Set Programming as Constructive Proof Search
• First-order unification in the PVS proof assistant
• scientific article; zbMATH DE number 3992945 (Why is no real title available?)
• scientific article; zbMATH DE number 4114588 (Why is no real title available?)
• Proof Search for the First-Order Connection Calculus in Maude
• A First Order Extension of Stålmarck’s Method
• Artificial Intelligence and Symbolic Computation
• Theorem Proving in Higher Order Logics

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 Q3496309)