**clnat** is a prover for *Classical propositional
logic* based on the natural deduction calculus **Ncr** presented in

M. Ferrari and C. Fiorentini. Proof-search in natural deduction calculus for classical propositional logic. In H. De Nivelle, editor,TABLEAUX 2015, LNCS, vol. 9323, pages 237–252. Springer International Publishing, 2015. [DOI]

Download the `clnat-1.0.jar` file.

Note

`clnat-1.0.jar` requires Java 1.8 or later. The LaTeX files
generated by the application depend on the packages `tikz`,
`xifthen` and `proof` available at CTAN.

Run the `clnat-1.0.jar` file using the following command:

`$ java -jar clnat-1.0.jar [options] [problem file]`

where *[problem file]* (optional) is the file containing the problem description
and *[options]* is a list of options. If the problem file name is not specified
the *-i* option must be specified.

Run:

`$ java -jar clnat-1.0.jar -h`

for a detailed description of available options.

Formulas must be specified using the following syntax:

```
Syntax of formulas
atoms: Java identifiers
logical: false, & (and), | (or), ~ (not), -> (implies), <=> (iff)
notes: (~ A) is translated as (A -> false)
(A <=> B) is translated as ((A -> B) & (B -> A))
```

A **problem description** is a file describing an input problem. It
contains the formulas describing the problem and, possibly, other
informations as its name and its provability status.

The prover supports three problem descriptions.

A plain problem description is a file consisting of only one line
specifying the formula to prove. To provide such a file as input use
the `-r plain` option. As an example, the following is a plain
specification of the double negation of the tertium-non-datur
principle.

```
~(~(p | ~p))
```

A **JTabWb** problem description is a file having the following
structure:

```
%------------------------
% Formula : name
% Status : provable|unprovable
%------------------------
formula
%------------------------
```

where:

*name*is the name of the formula;*status*specifies if the formula is*provable*or*unprovable*;*formula*is a formula.

To provide such a file as input use the `-r jtw` option.

As an example, the following is the specification of above problem in JTabWb-format:

```
%------------------------
% Formula : double-negation-tertium-non-datur
% Status : provable
%------------------------
~(~(p | ~p))
%------------------------
```

Some problems specified in the JTabWb format are available in
`cpl_examples_jtabwb.zip`.

Running the prover in non-verbose mode, we get a summary describing
the essential facts about the performed proof-search. For example,
running **clnat** on the *Peirce law*, we get:

```
$ java -jar clnat-1.0.jar wffs/cpl_examples_jtabwb/peirce.jatbwb
** Reader [jtawb_format]
> Parsing problem... time (ms) [0]
** Problem [Peirce], status [PROVABLE]
> Building initial node set... time (ms) [108]
** Prover [cln 0.1]
> Proving...
****************************************************************
** Prover [cln 0.1]
** Problem [Peirce], status [PROVABLE], proof-search [SUCCESS], test [PASSED]
** Generated nodes [7], restored backtrack-points [0], restored branch-points [1]
** Timings (ms): PS (proof-search) [10], NSC (initial node set) [108], PP (problem parsing) [0]
** Proof time (PS + NSC + PP): (ms) [118]
****************************************************************
```

The first part of the report describes the actions performed the prover (input parsing, initial node set construction, proof-search). When the proof-search terminates the prover provides details about the performed proof search. In particular the second line describes the result of the proof-search on the given input problem:

*status*is the status of the input problelm (`PROVABLE`,`UNPROVABLE`or`UNKNOWN`).*proof-search*is the status of the proof-search (`SUCCESS`or`FAILURE`).*test*is`PASSED`if the status of the formula match the result of the proof-search and`FAILED`otherwise.

The following lines provide details on the prover execution (number of gnerated nodes, restored backtrack-points and restored branch-point) and execution times.

Running the **clnat** prover on a classically unprovable formula the
prover provides the description of a counter model of the initial goal.

```
$ java -jar clnat-1.0.jar wffs/cpl_examples_jtabwb/ref1.jtabwb
** Reader [jtawb_format]
> Parsing problem... time (ms) [1]
** Problem [ref1], status [UNPROVABLE]
> Building initial node set... time (ms) [111]
** Prover [cln 0.1]
> Proving...
****************************************************************
** Prover [cln 0.1]
** Problem [ref1], status [UNPROVABLE], proof-search [FAILURE], test [PASSED]
** Generated nodes [8], restored backtrack-points [0], restored branch-points [2]
** Timings (ms): PS (proof-search) [10], NSC (initial node set) [111], PP (problem parsing) [1]
** Proof time (PS + NSC + PP): (ms) [122]
****************************************************************
The goal
==>[UP]
((c -> (a | b)) -> ((q | r) -> r)) ;
is unprovable. A countermodel is [q].
```

Read more: *Verbose mode*.