Do you have a favorite non-classical logic, extending CL+, the positive fragment of classical logic? Or perhaps you have just invented a new logic by adding new axioms to a Hilbert-style axiomatization of CL+? You like your new logic, yet feel frustrated by the lack of analytic sequent calculi for your logic, or the fact that it has no intuitive and simple semantics? Then our system Paralyzer is just the right tool for you!
Paralyzer (PARAconsistent logics AnaLYZER) is a tool for tranforming Hilbert-style calculi (of a certain general form) into equivalent analytic sequent calculi, and generating an effective finite-valued semantics for them. Moreover, an encoding of the new calculi in the generic proof assistant Isabelle is produced. 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 input calculi of Paralyzer are obtained
(i) by extending the language of the positive fragment of classical logic, to a
language which includes also a finite set of new unary connectives, and
(ii) by adding to a Hilbert axiomatization of classical logic axioms over the new
language of a certain general form, which is defined in the paper [1].
You are just several clicks away from obtaining new exciting insights into your favorite non-classical logic...
For more information, please have a look at the tab "Using Paralyzer"!
The input axiom may consist of:
Moreover, the axiom has to satisfy the following conditions: For some subformula
*p1 (*(* p1) or *(p1 o p2), resp.) arising from the start symbol Rp (R1 or R2,
resp.), this subformula must not be contained
(i) in a positively occurring (sub)formula of the form (phi & psi), and
(ii) in a negatively occurring (sub)formula of the form (phi v psi) or (phi -> psi).
The check whether the axiom falls into the class and satisfies this condition will automatically be performed by Paralyzer!
*1(*1 a) -> a; (*2 a & *2 b) -> *2(a -> b); *2 a -> *2(a v b); *1(a & b) -> (*1 a v *1 b) ...Note that you can compute several axioms at once by concatenating them with ";"!
BK is a system over {&, v, ->, negation, circle}. Its corresponding sequent calculus extends LK+ with the predefined rules
for negation (*1) and circle (*2) (Note that in case you choose BK as the basic system, Paralyzer can exploit
the invertibility of the rules of circle to produce simpler rules.). For more information on BK, see also [2].
Paralyzer 1.2 is available for free as a tarred archive:
The input axiom may consist of:
*1(*1 a) -> a; (*2 a & *2 b) -> *2(a -> b); *2 a -> *2(a v b); *1(a & b) -> (*1 a v *1 b) ...
By extending the positive fragment of LK with unary connectives *1 and *2, Paralyzer computes:
You can also use the output of Paralyzer in the tool Gen2Sat, which is a tool for deciding derivability in a given analytic propositional pure sequent calculus.
The people currently involved in the development of Paralyzer are:
For more information, requests or suggestions, please contact Lara Spendier (lara [at] logic [dot] at), who is the author of Paralyzer.