TINC - Paralyzer

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

Input Syntax

For more information, please have a look at the tab "Using Paralyzer"!

The input axiom may consist of:

  • the letters a, b for atomic formulas
  • logical connectives:
    • & ... and
    • v ... or
    • -> ... implication
    • *1, *2 ... unary connectives
and it is generated by the following grammar:
  • S := Rp | R1 | R2
  • Rp := Rp o P1 | P1 o Rp | * a
  • R1 := R1 o P1 | P1 o R1 | * (* a)
  • R2 := R2 o P2 | P2 o R2 | * (a o b)
  • P1 := P1 o P1 | * a | a | b
  • P2 := P2 o P2 | * a | * b | a | b
  • o := &, v, ->
  • * := *1, *2

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!

Examples

  *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 ";"!

LK+ and BK

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].

Below you can choose whether to start with LK+ or the sequent calculus for BK and then submit the axiom(s).

Start with LK+ (no predefined rules for *1 and *2).
Start with the sequent calculus for BK:
Rules
Input Axiom:   

Paralyzer 1.2 is available for free as a tarred archive:

Input Syntax, Grammar & Examples

The input axiom may consist of:

  • the letters a,b for atomic formulas
  • logical connectives:
    • & ... and
    • v ... or
    • -> ... implication
    • *1, *2 ... unary connectives
and it is generated by the following grammar:
  • S := Rp | R1 | R2
  • Rp := Rp o P1 | P1 o Rp | * a
  • R1 := R1 o P1 | P1 o R1 | * (* a)
  • R2 := R2 o P2 | P2 o R2 | * (a o b)
  • P1 := P1 o P1 | * a | a | b
  • P2 := P2 o P2 | * a | * b | a | b
  • o := &, v, ->
  • * := *1, *2
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!

Examples for axioms are:
 *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) ...

Output of Paralyzer

By extending the positive fragment of LK with unary connectives *1 and *2, Paralyzer computes:

  1. Logical rules equivalent to the axioms given as input. In the generated rules G and D stand for the contexts.
  2. The set of truth values V_M for the PNmatrix corresponding to the generated calculus (with the predefined connectives *1 and *2, if selected).
  3. The truth tables for the connectives of the logic in input (that is &, v and -> and the new unary connectives)
  4. An encoding of the calculus for the generic proof assistant Isabelle that can be used for semi-automated proof search within the considered logic.

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.

  1. A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky, Automated Support for the Investigation of Paraconsistent and Other Logics, Proceedings of LFCS2013, LNCS7734, p. 119--133, 2013.

  2. A. Avron, B. Konikowska, and A. Zamansky. Modular construction of cut-free sequent calculi for paraconsistent logics. In 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), p. 85 - 94. 2012.

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.