Slaney's Logic F** is Constructive Logic
with Strong Negation
(Web Support)

Matthew Spinks and Robert Veroff

September 2009

This page provides Web support for

Slaney's Logic F** is Constructive Logic with Strong Negation [3].
In particular, we present here proofs that were found with the assistance of the program Prover9 [1].


In [2], Slaney et al. introduced a little-known deductive system F** in connection with the problem of the indeterminacy of future contingents. The main result of this paper shows that, to within definitional equivalence, F** has a familiar description: it is precisely Nelson's constructive logic with strong negation [4].

Prover9 Proofs

For each proof, we include input, output, proof and xml files created as follows.

prover9 -f > file.out

prooftrans -f file.out >

prooftrans xml -f file.out > file.xml

We note that these essentially are proof-checking runs, since they include steps from previously found proofs as hints. The original proofs were found using the method of proof sketches [5]. In particular, our approach was to find derivations with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired proofs.



  1. W. McCune. Prover9.
  2. J. Slaney, T. Surendonk and R. Girle. Time, Truth and Logic. Tech. Report TR-ARP-11/89, Automated Reasoning Project, Australian National University, Canberra, 1989. (gzipped postscript)
  3. M. Spinks and R. Veroff. Slaney's Logic F** is Constructive Logic with Strong Negation. Bulletin of the Section of Logic, to appear.
  4. D. Vakarelov. Notes on N-lattices and Constructive Logic with Strong Negation. Studia Logica, 36:109-125, 1977.
  5. R. Veroff. Solving Open Questions and Other Challenge Problems Using Proof Sketches. Journal of Automated Reasoning, 27(2):157-174, 2001. (postscript)