.. index:: single: fcube
.. _fcube/0:

.. rst-class:: right

**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:**
|    :ref:`integer <integer/0>`
|    :ref:`list <list/0>`
|    :ref:`os <os/0>`
|    :ref:`set <set/0>`
|    :ref:`user <user/0>`

| **Remarks:**
|    (none)

| **Inherited public predicates:**
|    (none)

.. contents::
   :local:
   :backlinks: top

Public predicates
-----------------

.. index:: gnu/0
.. _fcube/0::gnu/0:

``gnu/0``
^^^^^^^^^

Prints banner with copyright and license information.

| **Compilation flags:**
|    ``static``

| **Mode and number of proofs:**
|    ``gnu`` - ``one``


------------

.. index:: fcube/0
.. _fcube/0::fcube/0:

``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``


------------

.. index:: decide/1
.. _fcube/0::decide/1:

``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``


------------

.. index:: decide/2
.. _fcube/0::decide/2:

``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``