From Accessible Integrated Formal Reasoning Environments

The usability characteristics of the aartifact system's design can be leveraged within the context of other popular and well-established formal reasoning assistance and verification systems. The purpose of this project is to learn more about the Isabelle/Isar proof assistant and examine how it can interact with the aartifact system. In particular, we are interested in how the verification capabilities of Isabelle/Isar can be leveraged by aartifact to improve its own scope and confidence, and how the aartifact library and user interface can improve the experience of a user employing Isabelle/Isar.

Contents 1 Overview of Current Tasks 1.1 Task #1: Predicates and Propositional Logic 1.2 Task #2: How to Use Isabelle/Isar to Assemble Proofs 1.2.1 Converting Derivation Trees into Isabelle/Isar Proofs 2 Other Tasks 2.1 Task #3: Aartifact Syntax 2.2 Task #4: Libraries 2.2.1 Finding and Using Basic Facts in the Isabelle/Isar Library

[edit] Overview of Current Tasks

The aartifact system is designed to support the construction of formal arguments that involve predicates and operators that deal with common mathematical constructs such as numbers, vectors, and sets. It is necessary to become familiar with how Isabelle/Isar handles such formal arguments. A good place to start is the documentation page.

[edit] Task #1: Predicates and Propositional Logic

Task Description: Program an algorithm that converts formulas in propositional logic into valid Isabelle/Isar proofs so that the validity of such formulas can be verified using Isabelle. It is sufficient to convert formulas that only contain operators and constants drawn from an adequate set (e.g. implication, contradiction, and parentheses).

[edit] Task #2: How to Use Isabelle/Isar to Assemble Proofs

Task Description: Learn how to convert a valid derivation tree in any first-order or higher-order logic into a valid Isabelle/Isar proof. One way to document progress on this task is to define (abstractly) a recursive algorithm that can convert a valid derivation tree into an Isabelle/Isar proof.

Become familiar enough with Isabelle/Isar to manually convert a valid derivation tree into a valid Isabelle/Isar proof. This knowledge is essential for constructing a general-purpose algorithm for assembling and generating Isabelle/Isar proofs from within the aartifact system.

[edit] Converting Derivation Trees into Isabelle/Isar Proofs

Derivation trees are constructed inductively from a small collection of logical inference rules. We can approach this task by abstractly defining a recursive algorithm for producing Isabelle/Isar proofs that contains a case for each possible inference rule that can be encountered in a derivation tree.

1. Implication-Elimination: Consider the following logical inference rule.

[Impl-Elim]

By our induction hypothesis, we assume that we have already constructed Isabelle/Isar proofs and concluding and . How do we assemble a proof concluding ? It would be ideal to have the concrete Isabelle/Isar syntax with some placeholders into which the proofs and could simply be inserted.

Complete this task for the following inference rules: introduction of implication, disjunction, and conjunction; elimination of implication, disjunction, and conjunction; introduction of existential quantifiers; and elimination of universal quantifiers.

The elimination of existential quantifiers and the introduction of universal quantifiers can be ignored for now because these are not needed for the purposes of proof generation from within aartifact.

[edit] Other Tasks

The following tasks will be adjusted and will become current once the above tasks are complete.

[edit] Task #3: Aartifact Syntax

In its most restricted form, the aartifact syntax for logical formulas and proofs (sufficient for propositional logic) is defined in the following way.

    <word> ::= a-zA-Z
 
 <formula> ::= [<word> <word> ... <word>]
             | <formula> and <formula>
             | <formula> or <formula>
             | <formula> implies <formula>
             | not <formula>
             | { <formula> }
 
 <statement> ::= Assume <formula>.
               | Assert <formula>.
 
 <argument> ::= <statement> ... <statement>

The following Haskell data type can be used to represent this as abstract syntax.

   data Formula = Pred [String]
                | Formula `And` Formula
                | Formula `Or` Formula
                | Formula `Implies` Formula
                | Not Formula
 
 data Statement = Assume Formula
                | Assert Formula
 
  data Argument = Argument [Statement]

How would the corresponding constructs be encoded using Isabelle/Isar?

This article has examples of Isabelle/Isar propositional logic proofs starting around page 3. Below is an example:

 lemma "A -> A"
 proof
   assume a: A
   show A by (rule a)
 qed

Is it possible to introduce user-defined predicates and assemble formulas and proofs in propositional logic? How would an automated translation from the above syntax into Isabelle/Isar syntax be constructed (i.e. using Haskell)? In order to generate valid Isabelle/Isar syntax, it may be necessary to automatically introduce explicit names for assumptions and annotations for assertions that justify logical steps. It will be necessary to keep track of this information inside a variable throughout the recursive calls.

[edit] Task #4: Libraries

The aartifact system's usability stems in part from the incorporation of a large library of formulas dealing with common concepts. The Isabelle system is accompanied by a variety of libraries dealing with many mathematical concepts.

Can a static context for aartifact be derived from any Isabelle/Isar libraries dealing with numbers and sets in an automated fashion? One important distinction is that we are not interested in the actual proofs found in the Isabelle/Isar libraries, but the statements of those proofs.

One possible conclusion of this task may be that the libraries are not in a useful format for our purposes.

[edit] Finding and Using Basic Facts in the Isabelle/Isar Library

Suppose we want to write arguments that utilize basic facts about the inequality relations () on naturals, integers, or rationals. For example, we may want to construct the following argument:

 Introduce $x,y,z$.
 Assume $x < y$.
 Assume $y < z$.
 Assert $x < z$.

The following questions need to be answered:

1. How do we write an equivalent Isabelle/Isar proof?
2. What representation is used to encode facts such as ""? Can this be automatically converted to aartifact syntax?