Nonclassical Proofs: Theory, Applications and Tools

This research project crosses the boundaries between proof theory - which is an important branch of mathematical logic since the work of Hilbert - universal algebra, and theoretical computer science. It aims to establish the foundations for the theory of proofs in logics different from classical, boolean, logic. These logics (nonclassical logics) provide languages for reasoning e.g., about knowledge, time, dynamic data structures, vague information, resources, algebraic varieties and as such they are increasingly applied in various disciplines. Among them artificial intelligence, mathematics and computer science, where most of these logics actually originated. Nonclassical logics are usually introduced or described in a declarative way in the proof framework due to Hilbert and Frege. The resulting systems are, however, extremely cumbersome when it comes to finding or analyzing proofs. Moreover, a Hilbert-Frege system does not help answering useful questions about the formalized logic and the corresponding algebraic structure, such as `Is the logic decidable?` or `Does the algebra satisfy amalgamation or a certain order theoretic completion?`. These tasks call for algorithmic presentations of logics especially in the form of analytic calculi. Analyticity is crucial here since proofs in such calculi proceed by a stepwise decomposition of the objects to be proved (praedicatum inest subjecto - Leibniz). The introduction of analytic calculi for nonclassical logics is currently logic-tailored and the solutions to fundamental questions about these logics (decidability, complexity, â) and related algebras are searched on an individual basis. We aim to develop theoretical and engineering tools for automatically extracting analytic calculi for nonclassical logics from Hilbert-style systems. The resulting tools will be further exploited to systematically investigate nonclassical logics. Various results, currently proved in a logic-tailored fashion, will be established in a uniform way for large classes of logics. Our focus will not be on particular calculi, logics or algebras, but on general and uniform results whose instantiations are expected (i) to help logic users in the spirit of `logic engineering`, and (ii) to solve open questions on specific logics, calculi or algebras. Some benefits of our investigation are: Systematization of the field. This will change the focus of future investigations Progress on important and long standing open problems in proof theory, complexity of logical systems and universal algebra Classification of proof frameworks. This will support the discovery of connections and properties outside logical formalisms; it will also put some highly desired order into the jungle of formalisms that have been introduced to define analytic calculi for various logics New insights into classical logic are to be expected from a better understanding of nonclassical logics The main methodology to achieve the ambitious project`s aims will be the integration of proof theoretic and algebraic techniques (algebraic proof theory). Algebraic proof theory has already led to important results both in proof theory and in algebra and has the potential to become an independent and prominent research field.

Logic studies the principles of correct reasoning. It can be used to establish the correctness or the fallacy, for instance, of the reasoning employed by mathematicians when proving theorems, by physicians to make diagnoses, or by judges to take court decisions. Logic is also a foundation for defining the behaviour of "intelligent" machines, e.g. autonomous robots. The best known logic--classical logic--deals with statements that are either true or false. It can be used to formalize and reason about mathematical concepts or about circuits having only "on" and "off" states, but unfortunately it is not useful in all circumstances. For instance, it is ill-equipped to draw conclusions in the presence of fuzzy hypotheses (e.g. to simulate a medical diagnosis when various "degrees of pain" have to be considered), or to reason with norms, where the interest is not in what is true or false, but in what one should or should not do. In general, different reasoning contexts require different logics and this leads to non classical logics. Expressing reasoning using these logics via mathematical formulae allows us to unequivocally prove whether or not a certain line of reasoning, or a software program, is correct. Mathematical and computer-based tools are needed for this purpose. In the START project ``Non classical Proofs: Theory, Applications and Tools'' we investigated and developed these tools for large classes of non classical logics. As there are many useful non classical logics, and because practitioners in various areas keep introducing new ones as per their requirements, the emphasis was not on particular logics but on providing general and uniform results that apply to large classes of logics. We developed algorithmic presentations for various families of interesting and useful logics in the form of analytic calculi. These are formal systems that allows us to write proofs containing only formulas which are already in the formula to be proved. These calculi are the key to developing automated reasoning methods. The introduced analytic calculi were used to establish theoretical results about the involved logics which are important for application purposes in various areas (e.g., decidability, complexity bounds, interpolation, algebraic completions), and to develop new concurrent programming languages. The instantiation of our general results to specific cases also led to the solution of long-standing open problems for particular logics, calculi and algebras. Computer-based tools facilitating the investigation and use of non classical logics were also provided.