TINC - Tools for the Investigation of Non-Classical logics

Why non-classical logics?

Non-classical logics (i.e., logics different from classical, boolean logic) have found important applications in many fields like computer science or universal algebra. Intuitionistic, substructural, or paraconsistent logics are just a few cases in point - the importance of these logics has grown within the past few years as they are used in knowledge representation, formal verification, or artificial intelligence. By now, there are many interesting and useful non-classical logics and practitioners in various fields keep on introducing new logics to fulfill their needs.

Tools

We developed the following tools that implement theoretical results from our project Non-Classical Proofs: Theory, Application and Tools:

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
(i) transforms axioms of a certain form into equivalent analytic (hyper)sequent rules,
(ii) generates a paper containing the resulting analytic calculus, and,
(iii) if explicitly required by the user, checks whether Monoidal T-norm Logic MTL extended with the input axiom is standard complete.

Paralyzer

Paralyzer (PARAconsistent logics AnaLYZER) is a tool for tranforming Hilbert calculi (of a certain general form) into equivalent analytic sequent calculi, and generating an effective 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
(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.

Framinator

Framinator takes as input a frame condition specified in the language of first-order classical logic and transforms it - if possible - into an equivalent labelled sequent rule.

Framinator
(i) transforms frame conditions of a certain form into equivalent labelled sequent rules, and
(ii) generates a paper containing the resulting cut-free labelled calculus.

What is an analytic calculus?

By analytic calculus we mean a calculus whose proofs only consist of concepts already contained in the result.
The existence of such an analytic calculus for a logic is indeed a prerequisite for the development of automated reasoning methods and also key to establish essential properties of the formalized logic, such as consistency, decidability, or interpolation. However, discovering whether a logic has an analytic calculus is a challenging task which usually deserves a paper for each specific logic.

How to obtain an analytic calculus?

An analytic calculus for a logic is traditionally introduced by the following three steps:

    (i) A suitable formalism has to be chosen or invented, e.g. Sequent Calculus, Hypersequent Calculus, or the Calculus of Structure.
    (ii) Suitable rules for formalizing the logic under consideration have to be provided.
    (iii) Soundness, completeness and cut-elimination for the defined calculus have to be proved.

As these steps are all tailored to the particular logic at hand, and all three steps are very difficult to establish, many important logics still lack an analytic calculus. Hence, an automated procedure to introduce analytic calculi in a systematic and uniform way would be of great use for practitioners and scientists in various fields.

How to automatically obtain an analytic calculus?

The idea of an automated procedure for the introduction of analytic calculi is to select the right base system and extract suitable rules out of Hilbert axioms. Such a transformation procedure has first been introduced in [CGT08], where certain Hilbert axioms are transformed into equivalent analytic inference rules for sequent or hypersequent calculus. Since its introduction, the transformation procedure has been adapted for other classes of logic as well, see e.g. [CLSZ13] for paraconsistent logics, or [CR13] for display calculus.

Some references

[CGT08] A. Ciabattoni, N. Galatos and K. Terui. From axioms to analytic rules in nonclassical logics.
       IEEE Symposium on Logic in Computer Science (LICS'08), IEEE pp. 229-240, 2008.
[CLSZ13] A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky. Automated Support for the Investigation of Paraconsistent and Other Logics.
       Proceedings of the Symposium on Logical Foundations in Computer Science 2013 (LFCS). S. Artemov and A. Nerode (Eds.), LNCS, 2013.
[CR13] A. Ciabattoni and R. Ramanayake. Structural extensions of display calculi: a general recipe.
       In Proceedings of WoLLIC 2013, LNCS 8071, pp. 81-95, 2013.

What is standard completeness?

Standard completeness is completeness of a logic with respect to algebras based on truth values in [0, 1]. In a standard complete logic, connectives are interpreted by suitable functions on [0, 1], which makes it a fuzzy logic in the sense of [H98]. For example, conjunction and implication can be interpreted by a t-norm (the main tool in fuzzy set theory to combine vague information) and its residuum, or by classes of t-norms.

How to establish standard completeness?

Checking or discovering whether a logic is standard complete is sometimes a challenging task which deserves a paper for each specific logic. Traditionally, it is established by semantic techniques which are inherently logic-specific. Given a logic L described in a Hilbert system, semantic proofs usually consist of the following four steps:

    (i) The algebraic semantics of the logic is identified (L-algebras).
    (ii) It is shown that if a formula is not valid in an L-algebra, then it is not valid in a countable L-chain (linearly ordered L-algebra).
    (iii) It is shown that any countable L-chain can be embedded into a countable dense L-chain by adding countably many new elements to the algebra and extending the operations appropriately.
          This establishes rational completeness.
    (iv) Finally, a countable dense L-chain is embedded into a standard L-algebra, that is an L-algebra with lattice reduct [0; 1], using a Dedekind-MacNeillestyle completion.

The crucial step (iii) above (rational completeness) is the most difficult to establish as it relies on finding the right embedding, if any. A different approach to step (iii) is to use proof-theoretic techniques [MM07]. The idea is that the admissibility of a particular syntactic rule (called density) in a logic L can lead to a proof of rational completeness for L. Following this method, standard completeness for a logic L is established by

    (a) defining a suitable proof system HL for L extended with the density rule
    (b) checking that this rule is eliminable (or admissible) in HL, i.e. that density does not enlarge the set of provable formulas
    (c) obtaining standard completeness in many cases (but not in general) by means of the Dedekind-MacNeille completion.

A tool for checking standard completeness automatically

In [BCS12], steps (a)-(c) are automated for propositional logics extending Monoidal t-norm logic MTL [EG01] by Hilbert axioms of a certain form. Sufficient conditions on hypersequent rules, that ensure standard completeness for the formalized logics, are identified. The system AxiomCalc, which implements a systematic procedure for defining analytic hypersequent calculi for large classes of logics (step (a)), is extended to check the sufficient conditions which account for steps (b) and (c) at once. This allows for the computerized discovery of new fuzzy logics.

Some references

[BCS12] P. Baldi, A. Ciabattoni and L. Spendier. Standard completeness for extensions of MTL: an automated approach.
      In Proceedings of Workshop on Logic, Language, Information and Computation (WoLLIC), LNCS 7456, pp. 154-167, 2012.
[EG01] F. Esteva and L. Godo. Monoidal t-norm based logic: towards a logic for left-continuous t-norms.
       Fuzzy Sets and Systems, 124:271-288, 2001.
[H98] P. Hajek. Metamathematics of Fuzzy Logic, Kluwer. 1998.
[MM07] G. Metcalfe and F. Montagna. Substructural fuzzy logics.
      Journal of Symbolic Logic, 7(3):834-864, 2007.

What is an effective semantics?

By effective semantics we refer to a semantics that is inducing a decision procedure for its underlying logic. Examples of effective semantics are non-deterministic finite-valued matrices and partial Nmatrices (see [AL05,BLZ12]).

What are (partial) non-deterministic matrices?

Non-deterministic matrices (Nmatrices) [AL05] generalize the standard matrix semantics of logical systems. The truth-value of a formula is then chosen non-deterministically from a given set of options. While preserving all the advantages of ordinary many-valued matrices, Nmatrices can be applied to a wider range of logics. There are indeed many useful non-classical logics which have as semantics finite characteristic Nmatrices, but for which no finite many-valued characteristic matrices can be found.

Partial non-deterministic matrices (PNmatrices) [BLZ12] generalize the notion of non-deterministic matrices by allowing empty sets of options in the truth-tables of the logical connectives.

A tool for creating an effective semantics automatically

In [CLSZ13], we introduce the tool Paralyzer (and extend it in [CLSZ14]) for transforming Hilbert-style calculi (of a certain general form) into equivalent analytic sequent calculi, and generating an effective finite-valued semantics for them. Moreover, we create an encoding of the calculus for the generic proof assistant Isabelle that can be used for semi-automated proof search within the considered logic. 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 [CLSZ13].

Some references

[AL05] A. Avron, and I. Lev. Non-deterministic Multiple-valued Structures.
       Journal of Logic and Computation 15, 2005.
[BLZ12] M. Baaz, O. Lahav, and A. Zamansky. Effective finite-valued semantics for labelled calculi.
       In Proceedings of IJCAR’12, pages 52–66, 2012.
[CLSZ13] A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky, Automated Support for the Investigation of Paraconsistent and Other Logics.
       In Proceedings of the Symposium on Logical Foundations in Computer Science 2013 (LFCS). S. Artemov and A. Nerode (Eds.), LNCS, 2013.
[CLSZ14] A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky, Taming Paraconsistent (and Other) Logics: An Algorithmic Approach.
       Accepted, 2014.

  1. A. Ciabattoni and L. Spendier, Tools for the Investigation of Substructural and Paraconsistent Logics.
    In Proceedings of JELIA 2014. E. Ferme and J. Leite (Eds.), LNAI 8761, pp. 18--32, 2014.
  2. A. Ciabattoni, P. Maffezioli and L. Spendier, Hypersequent and Labelled Calculi for Intermediate Logics.
    In Proceedings of TABLEAUX 2013. D. Galmiche and D. Larchey-Wendling (Eds.), LNCS 8123, pp. 81--96, 2013.
  3. A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky, Taming Paraconsistent (and Other) Logics: An Algorithmic Approach.
    Accepted, 2014.
  4. A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky, Automated Support for the Investigation of Paraconsistent and Other Logics.
    In Proceedings of the Symposium on Logical Foundations in Computer Science 2013 (LFCS). S. Artemov and A. Nerode (Eds.), LNCS, 2013.
  5. P. Baldi, A. Ciabattoni and L. Spendier. Standard Completeness for Extensions of MTL: an Automated Approach.
    Workshop on Logic, Language, Information and Computation, LNCS 7456, pp. 154--167, 2012.

People currently involved in the development of TINC:

See also our project's web page: Non-Classical Proofs: Theory, Application and Tools.