Understanding Logic WiP coded in TPTP THF and TFF

Setup

Create a src directory to use as your TPTP HOME and set the TPTP environment variable with the absolute path:

mkdir src && cd src
export TPTP=$(pwd)
git clone git@github.com:CoreSenseEU/understanding-logic.git

This results in include() paths being read relative to the src directory. Other TPTP files can be placed in the same src directory matching this tree structure:

src
├── my_package
│   ├── example1.tff
│   ├── example2.thf
│   └── ...
└── understanding-logic
    ├── LICENSE
    ├── README.md
    ├── tff
    │   └── ...
    └── thf
        └── ...

Documentation

The documentation is available at https://coresenseeu.github.io/understanding-logic/.

The documentation is built using the Material for MkDocs framework, which allows for easy documentation generation from markdown files. While it is based on the CommonMark flavor of Markdown, many extensions are supported which add extra features such as Admonitions, Content Tabs, and Math to name a few.

To build it locally, see the Documentation Instructions.

Development Notes

Because Higher Order Logic (HOL) is not currently well supported in Vampire, any .thf files need to obey a few rules to avoid problems with their TPTP parser.

• Do not use builtin predicates or functiors ($distinct, $let, $ite).
• Do not use builtin theory axioms ($less, $greatereq, $floor, etc.).
• Do not use cannonical tff or fol formulas. You can convert them all to thf by rewriting functions and predicates with the @ operator between arguments. For example:

  tff(my_formula, axiom, my_function(v1, v2, v3) = v4).
  
  % -->
  thf(my_formula, axiom, ((my_function @ v1 @ v2 @ v3) = v4)).

Acknowledgement

This work has received funding from the European Union's Horizon Europe research and innovation programme under grant agreement No 101070254 (CORESENSE). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Commission. Neither the European Union nor the granting authority can be held responsible for them.