Object-Oriented Theorem Proving (OOTP): First Thoughts

TL;DR

This paper introduces object-oriented theorem proving (OOTP), a new style of automated theorem proving based on object-oriented programming, aiming to be as powerful and natural as traditional functional-based methods.

Contribution

It proposes OOTP as a novel generalization of traditional theorem proving, shifting from functional to object-oriented paradigms.

Findings

OOTP is a promising new style of ATP.

OOTP is as powerful as traditional theorem proving.

OOTP leverages object-oriented programming principles.

Abstract

Automatic (i.e., computer-assisted) theorem proving (ATP) can come in many flavors. This document presents early steps in our effort towards defining object-oriented theorem proving (OOTP) as a new style of ATP. Traditional theorem proving (TTP) is the only well-known flavor of ATP so far. OOTP is a generalization of TTP. While TTP is strongly based on functional programming (FP), OOTP is strongly based on object-oriented programming (OOP) instead. We believe OOTP is a style of theorem proving that is no less powerful and no less natural than TTP and thus likely will be no less practically useful than TTP.