scientific article; zbMATH DE number 3935002

MaRDI QIDQ3708773zbMATH OpenFDO

Authors Charles G. Morgan

Publication date 1985

zbMATH Keywords

implementationbackward proof tree generationlogics with modus ponensnon-resolutional theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Recommendations

• Automatic inductive theorem proving using Prolog
• scientific article; zbMATH DE number 4155933
• scientific article; zbMATH DE number 4061193
• scientific article; zbMATH DE number 63734
• scientific article; zbMATH DE number 1360950

Cited in

(24)

• Backward reasoning in systems with cut
• scientific article; zbMATH DE number 4033134 (Why is no real title available?)
• Automatic theorem proving and OTTER
• A nucleus of a theorem-prover described inAlgol-68
• Representing scope in intuitionistic deductions
• On flattening elimination rules
• The relevance of premises to conclusions of core proofs
• Cut for classical core logic
• Lazy techniques for fully expansive theorem proving
• Poitín: distilling theorems from conjectures
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• scientific article; zbMATH DE number 2000433 (Why is no real title available?)
• A complete semantic back chaining proof system
• On Theorem Proving in Annotated Logics
• scientific article; zbMATH DE number 3870638 (Why is no real title available?)
• The t‐variable method in gentzen‐style automatic theorem proving
• scientific article; zbMATH DE number 3992945 (Why is no real title available?)
• scientific article; zbMATH DE number 4007747 (Why is no real title available?)
• The applicability of logic program analysis and transformation to theorem proving
• Gentzen's proof systems: byproducts in a work of genius
• scientific article; zbMATH DE number 4061193 (Why is no real title available?)
• scientific article; zbMATH DE number 89224 (Why is no real title available?)
• scientific article; zbMATH DE number 1761418 (Why is no real title available?)
• A new application for explanation-based generalisation within automated deduction

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