full screen background image

Software

Tools for the Investigation of Non-Classical logics

The TINC system, which includes:

AxiomCalc

The system AxiomCalc takes as input an Hilbert axiom specified in the language of Full Lambek Calculus with exchange (i.e. intuitionistic logic without weakening and contraction) and transforms it, if possible, into an equivalent analytic sequent or hypersequent rule.

AxiomCalc

Link to the AxiomCalc software


Paralyzer

Paralyzer (PARAconsistent logics AnaLYZER) tranforms Hilbert calculi (of a certain general form) into analytic sequent calculi, and generates a (nondeterministic) finite-valued semantics for them. The method applies to a variety of well-known logics, including a large family of paraconsistent logics (and that is where the tool takes its name), as well as to other logics for which neither analytic calculi nor suitable semantics have so far been available.

The calculi of Paralyzer are obtained

Link to the Paralyzer software

Framinator

The system Framinator (FRAMe condItioNs Automatically TO Rules) takes as input a frame condition in the language of first-order classical logic provided by the user and transforms it - if possible - into an equivalent labelled rule.
Framinator

Link to the Framinator software