A Proof-of-Concept for Using PVS and Maxima to Support Relational Calculus

Abstract

<p> Mechanized mathematics systems, especially Theorem Provers (TP) and Computer Algebra Systems (CAS), can play a very helpful role in handling relational calculus. Computer Algebra Systems help to automate tedious symbolic computations. However, they lack the ability to make sophisticated derivations of logical formulas. Correspondingly, a Theorem Prover is powerful in deriving the truth-value of a logical formula. Nevertheless, it is not suitable for dealing with symbolic expressions.</p> <p> The main goal for our research is to investigate the automation of relational calculus using existing mechanized mathematics technologies. Particularly, we elaborated a heuristic that enables the assignment of tasks to PVS and Maxima to help perform relational calculus. As well we built a proof-of-concept tool that supports this calculus.</p> <p> To fulfill our objective, we adopted the following steps: 1. Investigated and evaluated the characteristics and capabilities of TPs and CASs. This step led us to select PVS and Maxima as the tools to be used by our system. 2. Explored a strategy that governs setting tasks to PVS and Maxima in order to perform relational calculus. Then, we propose a task assignment heuristic based on this strategy. 3. Designed and built a proof-of-concept tool that makes use of PVS and Maxima to help perform relational calculus. 4. Assessed our tool by using it to handle some illustrative examples of operations on concrete relations.</p> <p> In our work, relations are given by their characteristic predicates. We assume as well that predicates that are provided to our proof-of-concept tool are in a Disjunctive Normal Form. We adopt a linear notation for the representation of propositions, quantifications, and expressions. We fall short of providing a user interface, which makes the use of the tool that we built slightly difficult.</p>