A tableau-like representation framework for efficient proof reconstruction

DOI10.1007/10722086_31MaRDI QIDQ2721210zbMATH OpenFDO

Authors Stephan Schmitt

Publication date 1 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

analytic tableauxmatrix proofssequent proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Recommendations

• Proof reconstruction in classical and nonclassical logics (Diss., TU Darmstadt, 1999)
• Accelerating tableaux proofs using compact representations
• Deleting redundancy in proof reconstruction
• scientific article; zbMATH DE number 512980
• scientific article; zbMATH DE number 834573

Cited in

(3)

• Accelerating tableaux proofs using compact representations
• Proofs and reconstructions
• A framework for using knowledge in tableau proofs

Describes a project that uses

Uses Software

• Nuprl
• SETHEO
• leanTAP

This page was built for publication: A tableau-like representation framework for efficient proof reconstruction

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