clnat

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]

Running the prover

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.

Specifying input

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))

Problem description

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.

Plain problem description

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))

JTabWb problem description

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.

Output explanation

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.