Improving Automation for Higher-Order Proof Steps

Antoine Defourné (1, 2)

1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
2 MOSEL - Proof-oriented development of computer-based systems

We have extended the TLA+ proof system TLAPS with a new backend to improve the automation of proof steps that involve higher-order reasoning. The current support for such steps is poor, requiring the user to break down proofs into unnecessarily small steps. We defined a translation from TLA+ to THF, the TPTP dialect for higher-order logic, and evaluated several higher-order solvers on proof obligations generated from the standard library of TLA+. Our results demonstrate that the solvers are able to handle much coarser proof steps than the other strategies provided by TLAPS, reducing the amount of necessary user interactions by a significant margin.

Mots clés: Automated Deduction; Higher-Order Theorem Proving; TLA +; TLAPS

Domaines: Informatique et langage [cs.CL]; Logique en informatique [cs.LO]; Logiciel mathématique [cs.MS]; Langage de programmation [cs.PL]; Théorie et langage formel [cs.FL]

Antoine Defourné. Improving Automation for Higher-Order Proof Steps. FroCos 2021 - 13th International Symposium on Frontiers of Combining Systems, Sep 2021, Birmingham, United Kingdom. pp.139-153, ⟨10.1007/978-3-030-86205-3_8⟩. ⟨hal-03528009⟩