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