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.
We developed the following tools that implement theoretical results from our project Non-Classical Proofs: Theory, Application and Tools:
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.
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.
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.
[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.
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.
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.
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.
[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.
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]).
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.
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].
[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.
People currently involved in the development of TINC:
See also our project's web page: Non-Classical Proofs: Theory, Application and Tools.