scientific article; zbMATH DE number 1543300

MaRDI QIDQ4520767zbMATH OpenFDO

Authors Lawrence C. Paulson

Publication date 27 February 2001

Full work available at URL http://www.jucs.org/jucs_5_3/a_generic_tableau_prover

zbMATH Keywords

Isabelle

Mathematics Subject Classification ID

Recommendations

• The foundation of a generic theorem prover
• scientific article; zbMATH DE number 1088221
• First-order modal tableaux
• \textsc{MetTeL}: a tableau prover with logic-independent inference engine
• TABLEAUX: A general theorem prover for modal logics

Cited in

(24)

• α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
• A framework for using knowledge in tableau proofs
• A general tableau method for propositional interval temporal logics: theory and implementation
• Mechanized metatheory revisited
• Semi-intelligible Isar proofs from machine-generated proofs
• The Isabelle Framework
• Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
• Verifying the SET purchase protocols
• A proof-centric approach to mathematical assistants
• Effective normalization techniques for HOL
• scientific article; zbMATH DE number 4104409 (Why is no real title available?)
• Lightweight relevance filtering for machine-generated resolution problems
• On theorem prover-based testing
• Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
• From LCF to Isabelle/HOL
• Integration of formal proof into unified assurance cases with Isabelle/SACM
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Computational logic: its origins and applications
• Proving pointer programs in higher-order logic
• Automating automated reasoning. The case of two generic automated reasoning tools
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Automatic proof and disproof in Isabelle/HOL
• Automation for interactive proof: first prototype
• AUTO2, a saturation-based heuristic prover for higher-order logic

Describes a project that uses

Uses Software

• Isabelle/ZF
• TPTP
• Isabelle

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