Apia is a Haskell program for proving first-order theorems written in Agda using automatic theorem provers for first-order logic (ATPs). Before calling the ATPs, the Agda formulae are translated into TPTP language.
Apia is used for reasoning about functional programs by combining interactive and automatic proofs (see README.md).
Glasgow Haskell Compiler (GHC)
Apia supports the versions of GHC supported by Agda upstream, i.e. 7.10.3, 8.0.2, 8.2.2 and 8.4.3.
Check your version with:
$ ghc --version
Extended version of Agda
We have extended the development version of Agda in order to handle the new built-in ATP-pragma. This extended version of Agda is required by the Apia program.
ATPs: Apia can use offline or online ATPs
The currently supported offline ATPs are:
ATP | Tested version |
---|---|
CVC4 | CVC4 1.6 |
E | E 2.1 Maharani Hills |
Equinox | Equinox 5.0alpha (2010-06-29) |
ileanCoP | ileanCoP 1.3beta1 |
Metis | Metis 2.4 (release 20180301) |
SPASS | SPASS V 3.9 |
Vampire | Vampire 0.6 (revision 903) |
Z3 | Z3 version 4.5.0 - 64 bit |
Apia can use any online ATP available in the TPTP World by using the online-atps program.
The tptp4X program
The --check
command-line option or using
Z3 as a first-order ATP
require the tptp4X program from the
TPTP library. This program is included in
this repository. The tested version of tptp4X is 6.4.0.2 from
Geoff's Service Tools.
Extended version of Agda (see README.md)
The Apia program
You can download the Apia program using Git. The program can be downloaded and installed with the following commands:
$ git clone https://github.com/asr/apia.git
$ cd apia
$ cabal install
In order to test the installation of Apia, you can try to automatically prove the conjecture in
module Test where
data _∨_ (A B : Set) : Set where
inj₁ : A → A ∨ B
inj₂ : B → A ∨ B
postulate
A B : Set
∨-comm : A ∨ B → B ∨ A
{-# ATP prove ∨-comm #-}
using the E ATP by running the following commands:
$ agda Test.agda
$ apia --atp=e Test.agda
Proving the conjecture in /tmp/Test/9-8744-comm.tptp ...
E 2.1 Maharani Hills proved the conjecture
Apia will call the E ATP and tell if this ATP was able to prove the conjecture. If the ATP could not prove the conjecture after the default timeout, the process of proving that particular conjecture is aborted.
After installing the online-atps
tool from
this repository, it is
possible to use any ATP available on
SystemOnTPTP.
For example, we could use an online version of the E ATP using the following commands:
$ apia --atp=online-e Test.agda
Proving the conjecture in /tmp/Test/9-8744-comm.tptp ...
E-2.0 proved the conjecture
To see a list of all online ATPs available, run the following command:
$ online-atps --list-atps
We can run Apia using options set in YAML files with name .apia
.
The options break down into project-specific options in:
<project dir>/.apia
and non-project-specific options in:
~/.apia
-- for user non-project default optionsNote: When Apia is invoked outside a project it will source project specific
options from ~/.apia
. Options in this file will be ignored for a project with
its own <project dir>/.apia
.
Project-specific options are only valid in the .apia
file local to a
project, not in the user config files.
Note: We define project to mean a directory that contains an
.apia
file, which specifies valid options. The options are specified in thehelp
command. Checkapia --help
to see all options available.
In your project-specific options, you specify which options to use when running Apia.
We want to use the ATPs E, Metis and the online version of Vampire with Apia.
Also, we want to save the results in the directory /myoutputdir
and use
the option check
. Then, our Apia file should be similar to this one.
# cat ~/.apia
atp: ["e", "metis", "online-vampire"]
output-dir: "/myoutputdir"
check: true
Logical symbols
The following symbols are hard-coded, i.e. they should be used: ⊥
(falsehood), ⊤
(truth), ¬_
(negation), _∧_
(conjunction),
_∨_
(disjunction), the Agda non-dependent function type →
(implication), _↔_
(equivalence), the Agda dependent function type
(x : A) → B
(universal quantifier) and ∃
(existential
quantifier).
Agda version
The Apia program must be compiled using the same version of Agda that was used to generate the Agda interface files.