TRS Reasoning School

Note: TRS is an acronym for "TRS Reasoning School".

Warming up: Aug 24-28

[Resolution] Cláudia Nalon [Machine-Oriented Reasoning]

Reasoning Week: Aug 31-Sep 4

[ModRes] Cláudia Nalon [Modal Reasoning through Resolution]

[Prob] Marcelo Finger [Logic-Probabilistic Reasoning]

[Diag] Renata de Freitas [Diagrammatic Reasoning]

[Descr] Ivan Varzinczak [Reasoning with Description Logics]

[Verify] David Déharbe [Reasoning to Verify Computer Programs] - CANCELED

[NatL] Carlos Prolo [Reasoning with Natural Language]

[Approx] Benjamín Bedregal & Regivan Santiago [Approximate Reasoning]

[Proof] Björn Lellmann & Revantha Ramanayake [Proof-theoretical Reasoning]

[Compl] Edward Hermann Haeusler [Propositional Reasoning Complexity]

[PVS] Mauricio Ayala-Rincón [Formal Reasoning with PVS]

[Poly] Walter Carnielli [Reasoning with Polynomials]

[NMon] Christian Strasser [Non-monotonic Reasoning]

[Prag] Cassiano Terra Rodrigues [Pragmatic Reasoning]

[DProp] Frank Sautter [Dynamic Propositional Reasoning]

[Colour] Marcos Silva [Reasoning with Colours]

[NRefQ] Jonas Becker Arenhart [Non-Reflexive Logics in Quantum Reasoning]

Abstracts:

[Resolution] Machine-Oriented Reasoning (slides)

In 1965, John A. Robinson published the paper "A Machine-Oriented Logic Based on the Resolution Principle'', launching the basis for automated deduction as we now know it. The resolution principle combines unification on demand together with a cut-elimination rule, building on the theoretical works by Prawitz and Herbrand and also improving on previous automated heuristics for proof search developed by Davis-Putnam. The result is an elegant, easy to implement, sound, and complete proof procedure with only one inference rule for dealing with validity in First-Order logic. In this tutorial, we celebrate the 50th anniversary of Robinson's foundational work by looking at the theory behind resolution-based systems for classical logics (propositional and first-order), the main results concerning the theoretical and practical development of such systems, and the state-of-the-art heuristics that make of this proof procedure one of the most widely implemented and successful tools for Automated Reasoning.

[ModRes] Modal Reasoning through Resolution (slides)

Continuing the celebration of the 50th anniversary of J. A. Robinson's work on the resolution principle, in this tutorial we will examine resolution-based proof methods for propositional modal logics based on the axioms K, T, D, B, 4 and 5. We will briefly review the proof method proposed by Robinson for classical propositional logic as well as the basics of modal logics. We will discuss what needs to be taken into consideration when adapting the classical method to deal with the satisfiability problem for modal languages and look at two different resolution-based methods for families of mono-modal logics: the clausal method proposed by Mints and the non-clausal destructive procedure proposed by Fitting.

[Prob] Logic-Probabilistic Reasoning (slides: part 1 - part 2)

We present the intersection of Logical Reasoning and Probabilistic Reasoning, without any assumption of probabilistic independence. We present probabilistic logic from first principles, and relate the probabilistic version of problems with their classical version. We relate classical satisfiability (SAT) with probabilistic satisfiability (PSAT), and analyze how to bridge between these two forms of reasoning. We also discuss the interesting phenomenon: how come SAT and PSAT are both NP-complete if the latter is, or seems, so much more complicated than the former?

In the second part, we discuss issues related to Logic-Probabilistic modelling. We discuss how to compute a set of candidate solutions by minimizing an inconsistency measure between an initial distribution and a set of logic-probabilistic restrictions. Once we have a consistent distribution, we discuss on the Maximum a Posteriori (MAP) method of choosing "the" solution. We also discuss on the problems of defining measures of inconsistencies in probabilistic theories, and show its differences from measuring inconsistency in non-probabilistic theories. We finalize by discussing some applications.

[Diag] Diagrammatic Reasoning (slides)

Until the last century, with one possible noteworthy exception, diagrams were considered as just an aid to discovering and communicating mathematical theorems. Drawings could be used in thinking about math, but a proper proof of a theorem would be a text, a sequence of sentences. Usual logical systems use sentences (formulas) to represent information and inference rules are defined to "manipulate" such sentences. In the last two decades, however, various logical systems that use diagrams to represent information (instead of sentences) and, consequently, whose inference rules are defined to obtain diagrams from sets of diagrams, are designed and developed formally. The first soundness and completeness proofs for such a system, based on Venn diagrams, are due to Sun-Joo Shin (1995). In this tutorial I will present some examples of diagrammatic logics.

[Descr] Reasoning with Description Logics (slides: part 1 - part 2 - part 3)

This tutorial is an introduction to Description Logics in the context of knowledge representation and reasoning. Description Logics (DLs) are a family of logic-based knowledge representation formalisms with interesting computational properties and a variety of applications. In particular, DLs are well-suited for representing and reasoning about terminological knowledge and constitute the formal foundations of semantic web ontologies. There are many different flavors of description logics with specific expressiveness and applications, an example of which is ALC and on which we shall focus in this tutorial. The outline of the tutorial is as follows: We start with an introduction to the area of Knowledge Representation and Reasoning (KRR) and the need for representing and reasoning with terminological knowledge, which stands as the main motivation behind the development of DLs. We then present the description logic ALC, its syntax, semantics, logical properties and proof methods. Finally we illustrate the usefulness of DLs with the popular Protégé ontology editor, a tool allowing for both the design of DL-based ontologies and the ability to perform reasoning tasks with them.

[Verify] Reasoning to Verify Computer Programs

Being able to guarantee the correctness of a computer program is of paramount importance for the development of safety-critical systems with embedded software. This course will present a formal system of reasoning known as Hoare Logic that underlies many current program verification systems.

This course will be heavy on examples and light on theory.

[NatL] Reasoning with Natural Language (slides / movie transcripts)

"All men are mortal. Socrates is a man. Therefore, Socrates is mortal." This classical example of syllogism, for many attributed to Aristotle, has been used by many authors to illustrate how formal logical systems may be used to model natural language communication. In this tutorial, although we will indeed acknowledge that they constitute a fundamental basis to understanding how human language work, we will do it in a very critical, contrarian-like way, showing how logical inference systems break easily when naively applied to natural language reasoning.

In human dialogues, participants conventionally do not follow straightforwardly the inference models that one could naively try to impose on them. However, strangely enough, they are still aware of these models to different extents. An interesting intertwining between inferential logic, lexical contents, common sense, world knowledge, and other not so clearly understood aspects of language, which govern human communication, are also used in jokes, and give rise to fallacious arguments, misunderstandings, disputes, arbitration and, of course, funny robot talking in movies.

The main purpose of this tutorial is to arise in the students a taste for the challenges waiting to be tackled if we want some day to do automated processing of natural language in a minimally interesting way.

[Approx] Approximate Reasoning (slides)

The human reasoning has, in general, an approximate nature. For example, if you state: "If the night is very cold, then the majority of my guests will not attend my party". This sentence considers imprecise aspects and is not appropriately captured in a standard precise reasoning, in which thresholds must be fixed beforehand; e.g. below 10 Degree Celsius establishes that "Night is very cold" and the percentage which represents the "majority of my guests" is 51%.

Logic can be understood as the science or discipline which studies the formal principles of reasoning. In particular, Fuzzy Logic provides a precise framework to deal with such approximate reasonings. For us, approximate reasoning here means the process from which imprecise conclusions are deduced from imprecise premises. This deductive process is based on Fuzzy Logic, in which predicates are declared through the do called Linguistic Variables, the evaluation of sentences considers imprecise truth tables and the inference rules are graded.

In this tutorial we provide an overview of such framework.

[Proof] Proof-theoretical Reasoning (slides: parts 1 and 2 - part 3 - part 4)

Logic is concerned with the study and use of valid reasoning. The most well-known logics are classical propositional and first-order logic. Nevertheless, various other forms of reasoning are needed to model the different applications and situations that arise in practice, thus giving rise to many new logics distinct from classical logic. The study of these logics provides an understanding of the underlying applications and also leads to new solutions e.g. automated support. Important theoretical questions in this context include whether there is a procedure to decide if a given statement represents a valid inference in the logic or not (decidability), if decidable, then what is the optimal complexity of a decision procedure, the construction of focussing methods for effective proof-search, and questions regarding further meta-theoretic properties of the logic such as consistency or interpolation. The basis for the proof-theoretical approach to reasoning is the notion of proof in the logic, and in particular, the study of formal proof systems of the logic.

A major early achievement is Gentzen's introduction of the sequent calculus as a formal tool for studying the structure of proofs in classical and intuitionistic logic. The main result is the cut-elimination theorem which shows that proofs can be reduced to a normal form where the statement to be proved is constructed systematically from smaller statements. Gentzen used this result to give a proof of consistency of Peano arithmetic using a suitable induction principle. Subsequently, the sequent calculus has been adapted and used (together with a corresponding cut-elimination theorem) to prove meta-theoretical results for many modal and substructural (non-classical) logics that arise (and are applied) in diverse fields such as knowledge representation and to reason about multi-agent systems, resource-bounded programs and ethical problems.

In this tutorial, we introduce the sequent calculus and prove the fundamental cut-elimination theorem. Next we introduce normal and non-normal modal logics and substructural logics and corresponding sequent calculi and use the cut-elimination theorem to obtain meta-theoretic results such as decidability and complexity of proof search. We also consider the vexing question of how to introduce sequent calculi for new logics of interest, indicate the limitations of the sequent calculus and discuss generalisations such as hypersequent and labelled sequent systems that have been proposed in order to obtain proof-calculi with cut-elimination for larger classes of logics.

[Compl] Propositional Reasoning Complexity (slides)

The computational complexity of SAT and TAUT for purely implicational propositional logic is known to be PSPACE-complete. Intuitionistic Propositional Logic is also known to be PSPACE-complete, while Classical Propositional Logic is CO-NP-complete for Tautology checking and NP-complete for Satisfiability checking. We show how proof-theoretical results on Natural Deduction help analysing the Purely Implicational Propositional Logic complexity regarded its polynomial relationship to Intuitionistic and Classical Propositional Logics. The main feature in this analysis is the subformula property. We extended the polynomial reduction of purely implicational logic to any propositional logic satisfying the subformula property. We examine PROPOSITION I: Any propositional logic satisfying the sub-formula principle is in PSPACE. Using Proposition I, we: (1) Conclude that some well-known logics, such as Propositional Dynamic Logic and S5C (n = 2), for example, hardly satisfy the subformula property. On the other hand, these logics have proof procedures. They are seen to be mechanizable despite being EXPTIME-complete; (2) Show that finitely many-valued propositional logics are in PSPACE, and when they include the minimal implicational logic they are PSPACE-complete.

We point out some facts and discuss some questions on how the subformula property is related to the mechanization of theorem proving for propositional logics. The relationship between feasible interpolants and the subformula property is discussed. Some examples remind us that the relationship between normalization of proofs and the subformula property is weak. Finally we discuss some alternative criteria to consider a logic to be mechanizable.

The tutorial starts by a brief review of computational complexity.

[PVS] Formal Reasoning with PVS (slides - PVS exercises)

Among a great variety of proof assistants PVS has been chosen for this tutorial because its prover interface allows development of formal proofs that are very close to analytical proofs one can find in textbooks and papers. The objective of this tutorial is provide computer science, math and logic students and researchers with a general view about how reasoning techniques can be applied to formalize properties (presented as mathematical lemmas and theorems) related with the correct specification of computational objects (software and hardware). We hope this tutorial, on the one side, will bring a useful first view to undergraduate and graduate students about the use of proof assistants, in general, and, on the other side, an instrumental view of the application of PVS reasoning techniques, in particular, to researchers in formal methods.

[Poly] Reasoning with Polynomials (slides)

The method for automatic theorem proving proposed in my “Polynomial ring calculus for many-valued logics” (2005) is an algebraic proof mechanism based on handling polynomials over finite fields. Although useful in general domains, as in first-order logic, certain non-truth-functional logics and even in modal logics, the method is particularly apt for deterministic and non-deterministic many-valued logics, as will be shown in this tutorial. The term "polynomizing" refers to the uses of polynomial-like representations as a reasoning strategy and as a tool for scientific heuristics. I intend to show how proof-theory and semantics for classical and several non-classical logics, as well as algebrization of logics, can be approached from this perspective, and discuss the assessment of this prospect, in particular on what concerns recovering certain ideas of George Boole in unifying logic, algebra and the differential calculus.

[NMon] Non-monotonic Reasoning (slides: part 1 - part 2)

Defeasible reasoning is indispensable when dealing with a world full of uncertainties: we constantly draw conclusions that we may reject later in view of new information. For instance, when noticing that the streets are wet, I infer that it has been raining. However, once I discern that the roofs are not wet, I retract my previous inference. In situations like this, we make inferences from premises that do not warrant that our conclusions holds: they only warrant that the a conclusion is sufficiently likely. Defeasible reasoning is not restricted to everyday contexts. It is also abundant in the (pure and applied) sciences and in expert reasoning. E.g., when diagnosing a patient, John, who shows signs that best fit hyperthyroidism, a physician may conclude that John should be tested further for this condition. However, as soon as our physician is informed that John's thyroid has been removed, she will retract her previous inference. As these examples indicate, defeasible reasoning comes in many forms: we reason from effect to cause (abduction), we make generalizations (induction), we reason on the basis of what is normally or typically the case (default reasoning), we infer on grounds of the information our senses give us about our environment, etc. In order to explicate and evaluate such reasoning processes, formal methods were developed: nonmonotonic logics. In this tutorial we will discuss some central approaches in nonmonotonic logic.

[Prag] Pragmatic Reasoning (slides: part 1 - part 2)

The term “pragmatism” is usually held to mean an attitude completely devoid of theoretical concerns, thoroughly directed to sheer practical results. The very expression “pragmatic reasoning” would seem to be a contradiction from that perspective. Though common and widespread, it is a poor oversimplification. In order to understand why, this tutorial will deal with C.S. Peirce’s definition of pragmatic and pragmatism. Peirce is commonly regarded as the “father of pragmatism”, although he distanced himself from W. James and other self-proclaimed pragmatists. Peirce claimed his pragmatism derived from his readings of Kant, combined with his experimental laboratory training as a chemist and as an astronomer. In fact, his scientific training will allow him to abandon the subjectivist and idealistic tones from modern philosophy, and to make the sharp Kantian distinction between praktisch and pragmatisch not so sharp, thus blurring the boundaries between theoretical and practical reasoning. In this way, his treatment of abduction as a form of logically weak though heuristically strong reasoning, as well as his distinction between theorematic and corollarial kinds of deduction constitute the very core of his definition of pragmatism (or pragmaticism, as he at a certain point preferred) as the logic of discovery, and a form of methodeutics (not merely a method, but the method of methods). The topics to be presented in the tutorial are: a] Peirce’s (earliest) criticism of psychologism in logic; b] Logic and pragmatism in the context of his classification of the sciences of discovery; c] From kinds of reasoning to the method of science; d] Pragmatic reasoning and the possibility of metaphysics.

[DProp] Dynamic Propositional Reasoning (slides)

Three complementary approaches to formal logic can be distinguished: a static one, a kinematic one, and a dynamic one. The static approach investigates arguments in isolation; the kinematic approach investigates them in the framework of chains of arguments; and the dynamic approach investigates them in the framework of the interplay between the debaters. In this tutorial I will examine Classical Propositional Logic from a dynamic perspective. I will use extensively normal forms, and the notion of information will be used as the fundamental semantic notion. The following topics will be examined: 1) Static, kinematic, and dynamic approaches to formal logic; 2) Truth versus information; 3) Normal forms for Classical Propositional Logic; 4) Informational validity, strengthening, and weakening; 5) Types of opposition; 6) Enthymematic arguments; 7) Lush arguments; 8) Philosophy of logic behind the adopted approach.

[Colour] Reasoning with Colours (slides: part 1 - part 2)

Colours can be found in many central problems in the History of Philosophy: from Aristotle's examples for exclusions by contrariety and problems for the Principle of Excluded Middle to the collapse of Wittgenstein’s early Philosophy; from the discussion on the nature of secondary qualities in Modern Philosophy to more recent puzzles in the Hard Problem of Consciousness; from natural candidates for the synthetic a priori to the refusal of a sharp distinction between shape and content in Aesthetics. In this tutorial we will focus on some issues in History and Philosophy of Logic concerning the conceptual organization of colours. First, we will examine how some reasoning with colours has dramatically challenged Wittgenstein's influential Tractarian account of logic and how the so-called Colour Exclusion Problem has conducted his thoughts to a strong conventionalism about logical rules. Second, still regarding colour systems, we will explore some further questions about two philosophically relevant distinctions: i) between formal and material incompatibility and ii) between contradiction and contrariety.

[NRefQ] Non-Reflexive Logics in Quantum Reasoning (slides)

Quantum mechanics is widely regarded as presenting many challenges to orthodox forms of reasoning. Among some of those challenges, quantum theory is not only said to violate some form of the law of distribution in classical propositional logic but, also, according to some philosophers and popular accounts of the theory, to involve contradictions in some circumstances (for instance, in the case of Schrödinger’s cat, which is said to be dead and alive at the same time). In this tutorial, we shall focus on challenges presented by quantum theory to the concept of identity. Our first step is to present the main arguments advanced to the effect that quantum entities seem to violate traditional laws of identity as they are formalized in classical first-order logic with identity. According to an interpretation of the theory (which we shall discuss), quantum entities do not behave in complete agreement to those laws, and are typically called non-individuals. We shall also present a family of logics designed to deal with non-individuals, called non-reflexive logics. The most well-known system of such logics is quasi-set theory, with which we shall be mainly concerned. As a third goal, we discuss some difficulties advanced to the non-reflexive approach to quantum reasoning. The difficulties come from both logical as well as metaphysical perspectives.

Be sure to check the full detailed programme of NAT@Logic 2015 here!