<commit_before>tstp2agda [![Build Status](https://travis-ci.org/agomezl/tstp2agda.svg)](https://travis-ci.org/agomezl/tstp2agda)
====


A proof tool for translating TSTP proofs to [Agda] code.
Only [Metis](http://www.gilith.com/software/metis/) proofs for now.
Tested with Metis 2.3 (release 20160714).


## Installation

```
$ git clone https://github.com/agomezl/tstp2agda.git
$ cd tstp2agda
$ cabal install
```

## Usage

```
Usage: tstp2agda [OPTIONS] FILE

  -h       --help              Prints help message
  -o FILE  --output=FILE       Output to file      (default: STDOUT)
  -p NAME  --proof-name=NAME   Main proof name     (default: proof)
           --version           Show version number

```

## First proof reconstruction

Given a problem in TPTP format like this one

```
$ cd examples/problem
$ cat Basic-1.tptp
fof(a1,axiom,a).
fof(a2,axiom,b).
fof(a3,axiom, (a & b) => z).
fof(a4,conjecture,z).
```

we can get a proof in TSTP format using the Metis


```
$ metis --show proof Basic-1.tptp > Basic-1.tstp
$ cat Basic-1.tstp
---------------------------------------------------------------------------
SZS status Theorem for Basic-1.tptp

SZS output start CNFRefutation for Basic-1.tptp
fof(a1, axiom, (a)).

fof(a2, axiom, (b)).

fof(a3, axiom, ((a & b) => z)).

fof(a4, conjecture, (z)).
<commit_msg>[ README ] Fixed typo.<commit_after>tstp2agda [![Build Status](https://travis-ci.org/agomezl/tstp2agda.svg)](https://travis-ci.org/agomezl/tstp2agda)
====


A proof tool for translating TSTP proofs to [Agda] code.
Only [Metis](http://www.gilith.com/software/metis/) proofs for now.
Tested with Metis 2.3 (release 20160714).


## Installation

```
$ git clone https://github.com/agomezl/tstp2agda.git
$ cd tstp2agda
$ cabal install
```

## Usage

```
Usage: tstp2agda [OPTIONS] FILE

  -h       --help              Prints help message
  -o FILE  --output=FILE       Output to file      (default: STDOUT)
  -p NAME  --proof-name=NAME   Main proof name     (default: proof)
           --version           Show version number

```

## First proof reconstruction

Given a problem in TPTP format like this one

```
$ cd examples/problem
$ cat Basic-1.tptp
fof(a1,axiom,a).
fof(a2,axiom,b).
fof(a3,axiom, (a & b) => z).
fof(a4,conjecture,z).
```

we can get a proof in TSTP format using Metis


```
$ metis --show proof Basic-1.tptp > Basic-1.tstp
$ cat Basic-1.tstp
---------------------------------------------------------------------------
SZS status Theorem for Basic-1.tptp

SZS output start CNFRefutation for Basic-1.tptp
fof(a1, axiom, (a)).

fof(a2, axiom, (b)).

fof(a3, axiom, ((a & b) => z)).

fof(a4, conjecture, (z)).

{'fraction_non_alphanumeric': 0.20090805902383654, 'fraction_numerical': 0.022701475595913734, 'mean_word_length': 2.4927344782034346, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 9, 'https://': 6, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '34907', 'n_tokens_mistral': 1071, 'n_tokens_neox': 994, 'n_words': 258}