Object-Oriented Theorem Proving (OOTP): First Thoughts
Programming Languages
2019-02-28 v2
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.
Cite
@article{arxiv.1712.09958,
title = {Object-Oriented Theorem Proving (OOTP): First Thoughts},
author = {Moez A. AbdelGawad},
journal= {arXiv preprint arXiv:1712.09958},
year = {2019}
}
Comments
11 pages