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

### Location

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

**Marcelo Finger **

2.

**João Marcos (LoLITA / DIMAp, UFRN) **

3.

#### Download

#### Lecture Notes

4.

**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 *

5.

**Oswaldo Chateaubriand**

*PUC-Rio *

9h Lecture 4 - Leandro Suguitani

11h Lecture 3 - Walter Carnielli

14h Lecture 1 - Marcelo Finger

16h Lecture 2 - João Marcos

18h Ghost Speaker

11h Lecture 5 - Oswaldo Chateaubriand

14h Lecture 1 - Marcelo Finger

16h Lecture 2 - João Marcos

18h Ghost Speaker

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:

Abstracts:

Satisfiability and Probabilistic Satisfiability

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.

2.

Foundations of Computerized Theorem Proving

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.

3.

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.

** Topics: **

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

** JUAN C. AGUDELO**

State University of Campinas—UNICAMP and Eafit University

**WALTER CARNIELLI**

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)

Proof
theory for contemporary logic by handling polynomials over finite fields

**Walter Carnielli**

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

http://www.cle.unicamp.br/e-prints/vol_11,n_4,2011.html

4.

The algebraic tradition of logic and some relational systems

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.

5.

Logic, ontology, and epistemology

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)

Informs

Registration

Registrations are open for the XVI Brazilian Logic Conference/Logic School. - Registration

Registrations are open for the XVI Brazilian Logic Conference/Logic School. - Registration

**EBL** begins at 13h, on May 9th (Monday) and ends at 18h, on May 13th (Friday)

** LOGIC SCHOOL** begins at 9h, on May 7th (Saturday) and ends at 20h on May 8th (Sunday) See important dates:

Visa Informations

The Brazilian Embassies and Consulates abroad maintain updated web sites, that provide information about visas and entry requirements, such as immunizations, depending on where you are coming from, as well as other practical information and health tips. Please take some time to review the entry requirements to avoid unpleasant surprises.

© 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:

Home | Description | Comittees | Program | Keynote Speakers | Turing Session | Call for papers | Submissions | Logic School | Registration | Proceedings | Touristic information

Siga o XVI EBL: