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
Copyright: Copyright 2012 Mauro Ferrari, Camillo Fiorentini, Guido Fiorino; Copyright 2020-2024 Paulo Moura
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