Logic School

Saturday, May 7th

Welcome 8h30min
9h Lecture 4 - Leandro Suguitani
11h Lecture 3 - Walter Carnielli
14h Lecture 1 - Marcelo Finger
16h Lecture 2 - João Marcos
18h Ghost Speaker

Sunday, May 8th

9h Lecture 4 - Leandro Suguitani
11h Lecture 5 - Oswaldo Chateaubriand
14h Lecture 1 - Marcelo Finger
16h Lecture 2 - João Marcos
18h Ghost Speaker


Auditório do Instituto de Química
R. Outeiro São João Batista
Campus do Valonguinho
Centro, Niterói, RJ

Visualizar Logic School em um mapa maior

Since the last edition of EBL, in 2008, the Logic School was incorporated to the Conference, aimed at undergraduate and graduate students interested in Logic and connected researches, but it is also open to anyone who may be interested. The Logic School will happen on the weekend beforehand the Conference, on May 7th -8th, 2011.

The lectures delivered in the Logic School will be the following:



Satisfiability and Probabilistic Satisfiability
Marcelo Finger

Part 1: Satisfiability (SAT)

We present the old problem of propositional satisfiability, the original NP-complete problem, together with recent developments that led to the capability of solving SAT problems with tens and even hundred of thousands of variables, discussing their theoretical relation to proof theory and empirical results such as phase transition, which allows us to present the strategy that Deolalikar employed in a recent (and not yet accepted) attempt to prove that P?NP.

Part 2: Probabilistic Satisfiability (PSAT)

The problem of Probabilistic Satisfiability was proposed by George Boole in 1854 and was rediscovered several times since. It lies at the intersection of Deductive and Probabilistic reasoning, but almost all approaches to deal with it were based on linear algebraic approach. We present new approaches to PSAT based on Logic and hybrid Logic-Algebraic, discuss algorithms, theoretical properties and empirical properties such as phase transitions.


Foundations of Computerized Theorem Proving
João Marcos (LoLITA / DIMAp, UFRN)

Part 1: The engineering of an extremely flexible Logical Framework

The recent historical development of computer assistants for doing formal deduction is outlined. The focus lies on *Isabelle*, one of the most popular and well-succeeded generic environments for implementing mathematical theories and logical systems, and for reasoning with them. The metalanguage of *Isabelle* is based on Church's Type Theory and its basic reasoning mechanism implements a natural deduction formalism for a higher-order logic in which implication, quantification and equality are used to deal with inference, variables and rewriting. A single reasoning principle is employed: higher-order resolution, based on higher-order unification. All such tools and concepts are to be explained and illustrated in this lecture.

Part 2: Teaching and experimenting with classical and non-classical logics

In this lecture, instead of concentrating on the plethora of deductive systems that come already implemented with the basic distribution of *Isabelle*, we'll show instead how *Isabelle* may be used _ab nihilo_ for the design and the practical use of deductive systems for a variety of known logics. We'll illustrate this possibility, initially, by the implementation of classical inference rules (propositional and first-order) in several formats: natural deduction, sequent-style, tableaux, hilbertian systems. Next, we'll illustrate the implementation of rules typical to non-classical logics, with an emphasis on labeled modal logics. In each case we'll see how the framework of *Isabelle* allows us to freely experiment with the definition of our deductive systems, as well as to prove theorems and check hypothetical conjectures within or about such systems.


Proof theory for contemporary logic by handling polinomials over finite fields

Walter Carnielli

The goal of the mini-course is to show that, by generalizing the usual Boolean approach to semantics by means of polynomials over finite rings (in particular, Galois fields), it is possible to represent semantics and proof theory for several truth-functional and non-truth-functional propositional logics, bringing back a unity between logic and algebra which vindicates some intuitions by Boole and Leibniz. As motivating examples, I will discuss completely elementary ways of proving in several many-valued, paraconsistent and modal logics obtained by handling multivariable polynomials over Boolean rings. Starting from an observation that finite functions (and even non-deterministic functions) can be represented as power series, the method naturally applies to certain logics which are uncharacterizable by finite-valued semantics (in particular to the LFI's, or "logics of formal inconsistency" and to some modal logics). The resulting method might be of interest for informatics and automatic proof procedures. Some challenging problems in connection to this approach, as extensions of the method to intuitionistic logic, to full quantified logic, to modal logics in general and to infinite-valued logics (as Lukasiewicz logic), as well as connections to abstract algebraic logic, will also be discussed.

1) Historical perspectives and an overview on Boolean algebra
2) Polynomial handling of Classical Propositional Logic
3) On overview on finite fields and rings
4) Combinatorial representations
5) Many-valued logics treated in polynomial terms: examples
6) LFIs (paraconsistent logic) treated in polynomial terms: examples
5) Modal logics treated in polynomial terms: examples
6) Syllogistic logic treated in polynomial terms
7) Open problems and perspectives


Polynomial ring calculus for modal logics: a new semantics and proof method for modalities
State University of Campinas—UNICAMP and Eafit University
State University of Campinas—UNICAMP and SQIG—IT

Proving Paraconsistent, Many-Valued and Modal Logics by Handling Polynomials: Some Perspectives on Polynomizing Logics
Walter Carnielli
IFCH/CLE - State University of Campinas - Brazil
ICR-CSC - University of Luxembourg - Luxembourg
Department of Informatics and Mathematical Modeling at the Technical University of Denmark (DTU)

Lecture Notes

Proof theory for contemporary logic by handling polynomials over finite fields
Walter Carnielli

CLE e-Prints vol. 11(4), 2011


The algebraic tradition of logic and some relational systems

Leandro O. Suguitani, Itala M. L. D'Ottaviano
Centro de Lógica, Epistemologia e História da Ciência (CLE), IFCH-Unicamp

Petrucio Viana
Departamento de Análise, IME-UFF

The algebraic tradition of logic and some relational systems

In the past, the study of logic evolved under the shadows of the aristotelian syllogisms for a long period of time. It was not before the 19th century that a "new" perspective began to be considered as an alternative approach to logic, on which abstract algebra had a predominant role. Since then, logic has not been limited only to the analysis of a catalogue of pre-arranged inferences (as in syllogisms) but it is possible to present it as an "algebraic calculus". G. Boole was one of the main contributors for this deviation from the aristotelian tradition. As it is well known, the "algebraic structure" that nowadays takes his name constitutes a powerfull mathematical tool with which one can "properly represent" the "propositional logic" (PL). Nonetheless, we know that PL is too "weak", in the sense that it deals basically with "logical conectives" and "propositions" ("zero-ary relations") only. In order to enlarge this mathematical frame of logic, so that it could include more than just the propositional fragment, for instance, a frame in which "extension" of aristotelian logic could be embraced, A. De Morgan, followed by C. S. Peirce, E. Schröder and others, developed their "relational systems", within which "binary relations" (sometimes higher order arity) could also be treated in an algebraic framework. One of the products of this approach to logic is the currently study of "relation algebras" (RA), introduced by A. Tarski. In these lectures we aim at (i) presenting a historical overview about the progress of these relational systems introduced by the mentioned authors, (ii) presenting some important results about RA (mainly those which have guided investigation over "new" relational systems), (iii) analysing some open problems and, finally, (iv) giving a general perspective on the important applications that theses systems may have in different fields, as for instance, computer science, philosophy of science and foundations of mathematics.


Logic, ontology, and epistemology

Oswaldo Chateaubriand

In this seminar I will discuss the question whether, and in what sense, logic can be considered an ontological theory. After drawing some connections between Aristotle’s conception of logic, Frege’s development of logic, and the further development of modern logic, I conclude that the character of modern logic is fundamentally metaphysical, in a sense that includes both ontology and epistemology. The ontological aspect of logic is related to Aristotle´s view concerning a first science that formulates the most general principles of reality as such. I see Frege’s development of higher order logic as a hierarchy of objects and concepts as a partial realization of Aristotle’s idea. The epistemological aspect of logic is related to the theory of logical deduction, and to the development of the axiomatic method as a methodological method for theoretical science, which also goes back to Aristotle and was greatly extended by the modern development of logic. As part of my discussion I also examine critically Quine’s opposing view that logic does not formulate general laws about the structure of reality, but that it is based on grammar and truth. I argue that in spite of his disclaimers, Quine’s conception of logic also depends on general metaphysical considerations.

Comitê Científico da Escola de Lógica:
Renata de Freitas (UFF)
Petrucio Viana (UFF)

© 2011 - XVI EBL - Brazilian Logic Conference / Logic School / May 7th – 13th, 2011 Contact us
Home | Description | Comittees | Program | Keynote Speakers | Turing Session | Call for papers | Submissions | Logic School | Registration | Proceedings | Touristic information

Siga o XVI EBL:
 Logotipo do You Tube Logotipo do Facebook Logotipo do Linkedin Logotipo Blog Logotipo do Twitter

Valid CSS!        CSS válido!       Valid XHTML 1.0 Transitional