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
Copyright: Copright 2012 Mauro Ferrari, Camillo Fiorentini, Guido Fiorino; Copyright 2022 Paulo Moura
License: GNU GPL 2.0 or later version
Compilation flags:
static, context_switching_calls
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