Some applications of Gentzen's proof theory in automated deduction

DOI10.1007/BFB0038693MaRDI QIDQ5053006zbMATH OpenOpenAlexFDO

Authors Michael Beeson

Publication date 26 November 2022

Published in Extensions of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bfb0038693

Mathematics Subject Classification ID

Logic programming (68N17) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 3976991
• Extensions of logic programming. International workshop, Tübingen, FRG, 8--10 December 1989. Proceedings
• A decision procedure for propositional N-Prolog
• Uniform proofs as a foundation for logic programming
• scientific article; zbMATH DE number 63752

Cited in

(11)

• scientific article; zbMATH DE number 4160159 (Why is no real title available?)
• Automatic derivation of the irrationality of \(e\)
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi
• Presenting intuitive deductions via symmetric simplification
• A resolution theorem prover for intuitionistic logic
• A decision procedure for propositional N-Prolog
• Hao Wang's contributions to mechanized deduction and to the Entscheidungsproblem
• scientific article; zbMATH DE number 5000964 (Why is no real title available?)
• Zeno: an automated prover for properties of recursive data structures
• Automated deduction. A basis for applications. Vol. 1: Foundations, calculi and methods

This page was built for publication: Some applications of Gentzen's proof theory in automated deduction

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