object

`fcube`

FCube: An Efficient Prover for Intuitionistic Propositional Logic.

Availability:

logtalk_load(fcube(loader))

Author: Mauro Ferrari, Camillo Fiorentini, Guido Fiorino; ported to Logtalk by Paulo Moura.
Version: 5:0:1
Date: 2024-03-14

License: GPL-2.0-or-later

Compilation flags:

static, context_switching_calls

Uses:

integer
list
os
set
user

Remarks:

(none)

Inherited public predicates:

(none)

Public predicates 

`gnu/0`

Prints banner with copyright and license information.

Compilation flags:

static

Mode and number of proofs:

gnu - one

`fcube/0`

Reads a formula and applies the prover to it, printing 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

`op(1100,xfy,v)`

Scope:

public

fcube

`fcube`