full screen background image


Tools for the Investigation of Non-Classical logics

The TINC system, which includes:


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.


Link to the AxiomCalc software


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


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.

Link to the Framinator software