Improving automation for higher-order proof steps

DOI10.1007/978-3-030-86205-3_8OpenAlexW3197407391MaRDI QIDQ831930

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)

Uses Software

• Satallax
• TLAPS
• FOOL

Cites Work

• Unnamed Item
• Unnamed Item
• The higher-order prover Leo-III
• A combinator-based superposition calculus for higher-order logic
• Extending SMT solvers to higher-order logic
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Satallax: An Automatic Higher-Order Prover
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Extensional Crisis and Proving Identity
• TLA +  Proofs
• How to Write a Proof
• Superposition with lambdas

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