Refined Logic: Proof Assistants for the Masses

26 December 2016

Motivation

As PL and logic enthusiasts, Siva Somayyajula and I embarked on a journey in Fall 2016 by taking Prof. Bob Constable’s course in applied logic at Cornell University, which was a small class of about 20 students. We discussed classic topics like logic systems, refinement rules, and formal methods, as well as newer ideas in the field, such as automated reasoning, proof assistants, and constructive type/logic systems.

For our final project for this class, Siva Somayyajula and I created a refinement logics framework. To be specific, our framework, known as refined-logic, enables students and researchers to implement proof assistants for their specific logics with relative ease.

Our goal is to provide a simple solution for these researchers that works at a level more than just a toy script. In particular, for people with their own proof calculi, refined-logic provides a simple way for them to input their calculus and be given an executable that serves as the proof assistant for that logic system. This circumvents the writing of unnecessary interpreters and proof assistants on the part of the researcher, which is ordinarily a huge time sink. This meta approach allows researchers to focus on their own important work rather than concerning themselves with tricky boilerplate code.

This type of proof calculus-based assistant generation can ultimately be quite helpful, even to students studying functional programming from an axiomatic standpoint for the first time, such as in Cornell’s very own CS 3110 course.

Paper

The details of this framework can be found in our paper on the refinement logics, which discusses a hypothetical implementation of this framework as well as a general implementation of constructive logics in OCaml, a functional programming language.

We discuss providing the rules for an example calculus in our framework. We elected to discuss propositional calculus and how to use its rules in this implementation to create a helpful proof assistant. We also provide instructions on how future work can extend this to first-order logic, which has more complicated governing axioms.

Implementation

We also have an implementation of the aforementioned framework, which again provides a generalized method of generating proof assistants for arbitrary proof calculi. We implemented the hypothetical propositional refinement calculus as an example, and left a similar implementation for first-order logic as an exercise for the reader. Future work can examine the set-up and structure of the code (which is adequately commented using interface files) to implement the proof calculi for custom logic systems.

We recently open-sourced our implementation of the framework. It is available as refined-logic on Github.