object

`fcube`

FCube: An Efficient Prover for Intuitionistic Propositional Logic.

Author: Mauro Ferrari, Camillo Fiorentini, Guido Fiorino; ported to Logtalk by Paulo Moura.
Version: 4:2:0
Date: 2022-10-08

License: GNU GPL 2.0 or later version

Compilation flags:

static, context_switching_calls

Uses:

integer
list
os
set
user

Remarks:

(none)

Inherited public predicates:

(none)

Public predicates 

`fcube/0`

Reads a formula and aplies the prover to it, priting its counter-model.

Compilation flags:

static

Mode and number of proofs:

fcube - one

`decide/1`

Applies the prover to the given formula and prints its counter-model.

Compilation flags:

static

Template:

decide(Formula)

Mode and number of proofs:

decide(++compound) - one

`decide/2`

Applies the prover to the given formula and returns its counter-model.

Compilation flags:

static

Template:

decide(Formula,CounterModel)

Mode and number of proofs:

decide(++compound,--compound) - one

Protected predicates 

(no local declarations; see entity ancestors if any)

Private predicates 

(no local declarations; see entity ancestors if any)

Operators 

`op(1200,xfy,<=>)`

Scope:

public

`op(1110,xfy,=>)`

Scope:

public

`op(1000,xfy,&)`

Scope:

public

`op(500,fy,~)`

Scope:

public

fcube

`fcube`