PHOLI - PARTIAL HIGHER-ORDER LOGIC WITH INTERFACES

Abstract

This project aimed to develop a light, easy-to-use proof-checking tool based on Partial Higher-Order Logic with Interfaces (PHOLI) calculus. The main goal was to create a system that automatically validates mathematical proofs and is not difficult to use like the other existing proof assistants. The project involved the design and development of a compact software prototype written in C++20. The system checks logical proofs by parsing formulas, verifying their validity, and presenting the results in human-readable form. Key accomplishments include the successful implementation of the parser, a pretty printer for terms and belief states, and the validation of several theorems. This work contributes to making formal proof verification more accessible to students and researchers by providing a simple tool that could be used in teaching and applied logic. The system was tested using various examples and proved to be correct. Future work will focus on developing an easy-to-use UI, type checker, and proof checker.