Improving automation for higher-order proof steps

DOI10.1007/978-3-030-86205-3_8MaRDI QIDQ831930zbMATH OpenOpenAlexFDO

Authors Antoine Defourné

Publication date 24 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-86205-3_8

zbMATH Keywords

automated deductionhigher-order theorem provingTLA\textsuperscript{+}TLAPS

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• Increasing the efficiency of automated theorem proving
• scientific article; zbMATH DE number 1552534
• Automating soundness proofs
• Automated constructivization of proofs
• scientific article; zbMATH DE number 107881
• scientific article; zbMATH DE number 3878393
• Automating the search for elegant proofs
• Proof simplification and automated theorem proving
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Publication:4934147

Cites work

• scientific article; zbMATH DE number 1390334 (Why is no real title available?)
• scientific article; zbMATH DE number 7471678 (Why is no real title available?)
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• A combinator-based superposition calculus for higher-order logic
• Extending SMT solvers to higher-order logic
• Extensional crisis and proving identity
• How to Write a Proof
• Satallax: An Automatic Higher-Order Prover
• Superposition with lambdas
• TLA +  Proofs
• The higher-order prover Leo-III

Cited in

(2)

• Automated Improving of Proof Legibility in the Mizar System
• How to make ad hoc proof automation less ad hoc

Describes a project that uses

Uses Software

• FOOL
• TLAPS
• Satallax

This page was built for publication: Improving automation for higher-order proof steps

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