Emar Maier

• Area: LaLo
• Level: I
• Week: 2
• Time: 14:00 – 15:30
• Room: C2.01

Abstract

We use language to talk about individuals, events, times, states of affairs, and possibilities, but we can also use it to talk about words, letters, sentences and utterances. In both formal and natural languages we find quotational devices dedicated to the latter function, i.e. using language to refer to linguistic entities.

Quotation is, however, not a unitary phenomenon. In addition to so-called pure quotation (“cat” has three letters), there is a family of related linguistic phenomena, all associated with quotation marks and/or metalinguistic reference of some kind. In this course I give an introduction to the semantics of quotational constructions in natural language.

After a broad, philosophically oriented overview of the various forms of quotation, I discuss in detail the semantics of pure quotation, direct and indirect discourse, and mixed quotation. Along the way we’ll discuss current debates involving “monsters”, Free Indirect Discourse (in literary narrative) and Role Shift (in signed languages).

The course will be accessible to most if not all ESSLLI participants. More specifically, prerequisites are some minimal familiarity with basic formal semantics, whether from linguistics, logic, or philosophy of language.

Outline

Lecture I: Pure Quotation

I survey the different forms of quotation before zooming in on pure quotation. I review the classic philosophical analyses (e.g. Quine 1940; Tarski 1933; Davidson 1979; Cappelen and Lepore 1997; Clark and Gerrig 1990), focusing specifically on issues related to the (non-)compositionality of pure quotation (Maier, 2014b).

Lecture 2: Direct and Indirect Discourse

I introduce the direct – indirect distinction in reported speech. I explore analyses of direct discourse as pure quotation, and of indirect discourse as an intensional operator (Kaplan, 1989; Zimmermann, 1991).

Lecture 3: Between Direct and Indirect Discourse

I discuss quotational phenomena that don’t fit within a rigid direct–indirect dichotomy. I focus on two that are currently hotly debated in formal semantics: the literary style known as Free Indirect Discourse (Banfield, 1982; Schlenker, 2004; Sharvit, 2008; Eckardt, 2014), and the modality specific form of reporting in signed languages known as Role Shift (Quer, 2005; Schlenker, 2014; Davidson, 2015). I’ll compare attempts at assimilating these phenomena into direct discourse, and into indirect discourse (using context shifting operators in extensions of Kaplan’s logic).

Lecture 4: Mixed Quotation

Mixed quotation combines aspects of direct discourse/mention and indirect discourse/use. I compare the main views in the ongoing debate about the semantics of this construction, including the current state of the art (Geurts and Maier, 2005; Potts, 2007; Shan, 2011; Maier, 2014a).

Lecture 5: Unquotation

I introduce the dual of mixed quotation, unquotation, in order to capture some remaining puzzles of mixed quotation. I then consider the possibility of extending the semantics of mixed quotation and unquotation to account for the phenomena discussed in Lecture 3, i.e. Free Indirect Discourse and Role Shift (Maier, 2015). Finally, I consider the relation between unquotation and so-called quotational indefinites (Sudo, 2013; Koev, 2015).

References

 

Slides

Lecture Notes / handout (all slides combined) in pdf

Nicolas Troquard

• Area: LaLo
• Level: I
• Week: 1
• Time: 17:00 – 18:30
• Room: C3.06

Abstract

The concept of action is an all-around topic of scholarly investigation. The formal aspects have long been studied by  philosophers. It is also a fundamental concept in the field of multiagent systems (MAS) whose main objective is the design of artificial agents who have to interact in an environment, by selecting a given course of action on the basis of their beliefs and preferences.

In computer science, Dynamic Logics (DL) are the archetypical logics to talk about the actions of computer programs. They are modal logics for representing the states and the events of dynamic systems. The language of DLs is both an assertion language able to express properties of computation states, and a programming language able to express properties of system transitions between these states. DLs permit to talk and reason about states of affairs, processes, changes, and results. For every program P, there is a modality <P> where<P>A means that “after P, it is possible that A is the case”.

On the other hand, another family of logics of agency prefers to abstract away from the process of action and concentrate itself on the result of the action. It includes Belnap and colleagues Seeing-To-It-That (STIT), and the logics of Bringing-It-About (BIAT) due to Kanger, Pörn, and others. They are modal logics where for each agent i there is a modality DOES_i where DOES_i A means that “i sees to it / brings about that A is the case”.

These modalities are versatile and can be usefully combined with other notions like time, obligations, beliefs. They find many natural applications in modeling and reasoning about processes, individual agency and collective agency.

This course is to provide a gentle overview to the logics of action and agency and of their applications.

Slides

Chapter 1: Introduction to agency

Chapter 2: Propositional Dynamic Logic and Theory of Action

Chapter 3: The modal view of agency

Chapter 4: Applications of agency to social influence and obligations

Chapter 5: Applications of agency to power

Jakub Szymanik

• Area: LaLo
• Level: F
• Week: 1
• Time: 17:00 – 18:30
• Room: D1.03

Abstract

Reasoning is one of the key aspects of human cognition. Traditionally logic was meant as a systematic theory of human reasoning, but in the 20th century the main developments in logic focused on mathematics and its foundations, and logic has been gradually replaced by more specific cognitive theories of reasoning. Still, these theories are mostly inspired by classical consideration of logic, probability, and computations. In this course we are going to particularly focus on the relationship between logical complexity and cognitive difficulty in reasoning

 

Tentative Outline

Topic 1: Syllogistic Reasoning;

Topic 2: Meaning and Complexity;

Topic 3: Social Reasoning;

Topic 4: Reasoning in Games;

Topic 5: Categorization;

This is a short monographic course discussing classic themes and recent developments in logic and cognitive science of reasoning. There are no prerequisites but it will mostly advantage students who are interested in logic, language, computations, and cognition. The course is planned to be self-contained and self-explanatory; reading the suggested bibliography prior to the course is not expected of the participants; questions and discussion are welcome during the lectures.

Slides

Available under this link: https://goo.gl/40Ws82

References

1. T. Braüner. Hybrid-Logical Reasoning in False-Belief Tasks, TARK 2013, Chennai, India.
2. N. Gierasimczuk, H. van der Maas, and M. Raijmakers. An analytic tableaux model for Deductive Mastermind empirically tested with a massively used online learning system, Journal of Logic, Language and Information, 2013.
3. B. Geurts. Reasoning with quantifiers. Cognition, 2003.
4. T. Icard III, and L. Moss. Recent Progress in Monotonicity. Linguistic Issues in Language Technology, 2014.
5. A. Isaac, J. Szymanik, and R. Verbrugge. Logic and complexity in cognitive science, Johan van Benthem on Logical and Informational Dynamics, A. Baltag and S. Smets (Eds.), Outstanding Contributions to Logic, 2014.
6. P. N. Johnson-Laird and S. Khemlani. Toward a unified theory of reasoning. The Psychology of Learning and Motivation, 2013.
7. P. N Johnson-Laird, S. Khemlani, and G. P. Goodwin. Logic, probability, and human reasoning. Trends in Cognitive Sciences, 2015.
8. D. Lassiter and N. Goodman. How many kinds of reasoning? Inference, probability, and natural language semantics. Cognition, 2015.
9. J. Macnamara. A border dispute: The place of logic in psychology, MIT Press, 1986.
10. J. Feldman. Minimization of Boolean complexity in human concept learning, Nature 2000.
11. M. Oaksford and N. Chater. Bayesian rationality the probabilistic approach to human reasoning. Oxford University Press, 2007.
12. N. Pfeifer. The new psychology of reasoning: A mental probability logical perspective. Thinking & Reasoning, 2013.
13. L.J. Rips. The psychology of proof. Cambridge, MIT Press, 1994.
14. K. Stenning and M. van Lambalgen. Human reasoning and cognitive science. MIT Press, 2008.
15. M. Tessler and D. Goodman. Some arguments are probably valid: Syllogistic reasoning as communication. In Proceedings of the Thirty-Sixth Annual Conference of the Cognitive Science Society, 2014.
16. R. Verbrugge, Logic and social cognition: The facts matter, and so do computational models. Journal of Philosophical Logic, 2009.

Eric Pacuit

• Area: LoCo
• Level: A
• Week: 1
• Time: 14:00 – 15:30
• Room: C2.01

Abstract

Social Choice Theory is the formal analysis of collective decision making. A growing number of logical systems incorporate insights and ideas from this important field. This course will introduce the key results (including proofs) and the main research themes of Social Choice Theory. The primary objective is to introduce the main mathematical methods and conceptual ideas found in the Social Choice literature. I will also pay special attention to recent logical systems that have been developed to reason about group decision making and how social choice-style analyses are being used by logicians.

Specific topics include:

• Proofs of key Social Choice results (e.g., Arrow’s Impossibility Theorem, Sen’s Impossibility of the Paretian Liberal, Müller-Satterthwaite Theroem, Harsanyi’s Utilitarian Theorem, and the Gibbard-Satterthwaite Theorem)
• Responses to Arrow’s Theorem (e.g., Domain Restrictions, such as Sen’s Value Restriction and Black’s Single-Peakedness Condition)
• Axiomatic characterizations of voting procedures (May’s Characterization of the majority rule, Maskin’s Characterization of majority rule, Fishburn’s Characterization of Approval Voting, Young’s Characterization of positional voting, Saari’s characterization of Borda Count)
• Voting paradoxes (e.g., Condorcet’s paradox, Anscombe’s Paradox, the No-Show Paradox)
• Generalizations of the classic framework (e.g., assuming there are infinitely many voters)
• Judgement aggregation (e.g., Dietrich-List impossibility theorem)
• The Condorcet Jury Theorem and its many variants
• Logics for reasoning about preference aggregation (modal logics for preference aggregation, dependence and independence logic for social choice theory).

The course will not only provide a broad overview of the field of Social Choice from a logicians perspective, but will also discuss key technical results of particular interest to logicians. The main goal is to provide a solid foundation for students that want to incorporate results and ideas from Social Choice Theory into their field of study. I will also explore the to what extent modal and preference logics can faithfully formalize key results in social choice theory.

Slides

Additional References

Thomas Icard

• Area: LoCo
• Level: A
• Week: 1
• Time: 09:00 – 10:30
• Room: C2.01

Abstract

The dominant normative theories of inference, reasoning, and decision making typically work at a level of abstraction that eclipses the resource limitations of actual, physically instantiated agents. Happily, this level of abstraction often results in the sorts of elegant theorizing familiar from logic, semantics, decision theory, game theory, and related areas. Meanwhile, practical business of computational implementation, concrete cognitive and linguistic modeling, and applications usually requires shortcuts, heuristics, and approximations to those normative theories, which often diverge quite radically from what is prescribed. Theorists across the disciplines have been well aware of this mismatch between theory and practice, at least since Herbert Simon’s seminal work. While there has been much ink spilt on the topic, as well as a number of promising research programs exploring bounded rationality from different perspectives, the theory of bounded rationality has not reached a consensus view.

The aim of this course is to cover some of the most successful and fruitful approaches to bounded rationality—from logic, artificial intelligence, cognitive science, and game theory—with an eye toward the possibility of unification. Topics will include:

• Classical perspectives by H. Simon and others.
• Bounded rationality in game theory (A. Rubinstein, etc.).
• Ecological approaches (G. Gigerenzer et al.).
• Bounded Optimality and Metareasoning in AI.
• Approaches inspired by ideas from thermodynamics and information theory.
• Applications of these ideas to methodological problems in cognitive science.

Slides

Additional References

Oleg Verbitsky

• Area: LoCo
• Level: A
• Week: 1
• Time: 14:00 – 15:30
• Room: C2.06

Abstract

We will study the relationship between the definability of graphs in first-order logic and the computational complexity of the graph isomorphism and homomorphism problems. If every graph in a class of graphs $C$ is definable with $k$ variables, then the isomorphism problem for $C$ is solvable in polynomial time by the $(k-1)$-dimensional Weisfeiler-Leman algorithm. Moreover, definability with finitely many variables and logarithmic quantifier depth implies that isomorphism can be tested even in parallel logarithmic time. The existential-positive fragment of $k$-variable logic corresponds to the algorithmic techniques for homomorphism testing (i.e., constraint satisfaction) known as $k$-Consistency Checking. Examining the expressibility of this logic, we are able to estimate the time efficiency of this approach to constraint satisfaction.

Slides

Part 1. Logical complexity of graphs: Basic definitions and examples.
Part 2. Isomorphism testing by Color Refinement and two-variable counting logic.
Part 3. The graphs definable with two variables and counting quantifiers.
Part 4. Two-variable counting logic and linear-programming methods.
Part 5. Two-variable counting logic and distributed computing.
Part 6. Existential-positive two-variable logic and Constraint Satisfaction.
Part 7. Alternation hierarchy of two-variable logic.
Part 8. Counting logic with 3 and more variables: Applications to isomorphism testing.

Additional References

• O.Pikhurko and O.Verbitsky. Logical complexity of graphs: a survey. In: Model Theoretic Methods in Finite Combinatorics. Contemporary Mathematics, Vol. 558, pages 129-179. American Mathematical Society (2011).
• V.Arvind, J.Köbler, G.Rattan and O.Verbitsky. Graph Isomorphism, Color Refinement, and Compactness. A combined version of conference papers in FCT’15 and MFCS’15.
• A.Krebs and O.Verbitsky. Universal covers, color refinement, and two-variable logic with counting quantifiers: Lower bounds for the depth.
  Proc. LICS’15, pp. 689-700 (2015).
• C.Berkholz and O.Verbitsky. On the speed of constraint propagation and the time complexity of arc consistency testing. Proc. MFCS’13, Vol. 8087 of LNCS, pp. 159-170 (2013).
• C.Berkholz, A.Krebs, and O.Verbitsky. Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy. ACM Transactions on Computational Logic 16, Article 21 (2015).
• M.Grohe and O.Verbitsky. Testing graph isomorphism in parallel by playing a game. Proc. ICALP’06, Vol. 4051 of LNCS, pp. 3-14 (2006).

Andreas Abel

• Area: LoCo
• Level: I
• Week: 1
• Time: 17:00 – 18:30
• Room: C2.01

Abstract

Type Theory has been developed as a foundation of mathematics and computer science by logicians
like Alonzo Church (from 1930) and Per Martin-Löf (from 1970). Suitable as a basis for computer-assisted proof, it is receiving increasing interest from mathematicians (e.g. Fields medalist Vladimir Voevodsky), information technology (e.g. for verifying compilers and operating systems), and computational linguistics (Aarne Ranta’s Grammatical Framework). Type theory is based on the Curry-Howard Isomorphism, which describes a precise relationship between proofs of a proposition and programs of the corresponding type. In this course, we will study the basics of Type Theory, and practice programming and proving in Agda, an implementation of Martin-Löf Type Theory. We will cover first-order logic, induction, and coinduction from a practical perspective, but we will also take a look behind the veil at the metatheory of Type Theory: Computational interpretation, models of Type Theory and the meaning of judgements, consistency and decidability of type-checking.

Agda Installation

To follow the Agda exercises, please install Agda.  For some systems, Agda might be packaged for easy installation (e.g. homebrew for Mac OS).  In general, an installation from source should be possible by the following steps:

• Install the emacs editor (if it is not already on your system).
• Install the GHC Haskell compiler with the cabal build system, preferably by getting the latest Haskell Platform.
• Add $HOME/.cabal/bin to your PATH (or wherever cabal will install binaries on your system).
• Install the latest versions of cabal-install, cpphs, alex, and happy from hackage.
cabal update
cabal install cabal-install
cabal install cpphs
cabal install alex
cabal install happy

• Install the latest version of Agda from hackage.
cabal install Agda
agda-mode setup

• The last command adds a search path to the emacs agda2-mode.el to your .emacs file.
  Launch emacs and open a new file HelloWorld.agda.
• Type in your first Agda code:
module HelloWorld where

• Check the file with Agda by pressing C-c C-l (Control-c Control-l) or selecting “Load File” from the Agda menu.

Slides

• Overview
• Lecture 1: Natural Deduction and the Curry-Howard Isomorphism
• Lecture 2: Dependent Types
• Lecture 3: Martin-Löf Type Theory
• Lecture 4: Agda (live-coding)
• Lecture 5: Coinduction (live-coding)

Further Lecture Material

• Scriptum for Natural Deduction and the Curry-Howard Isomorphism
• An LF representation of propositional logic in Agda

Additional References

• Per Martin-Löf. An intuitionistic theory of types: Predicative part. In Logic Colloquium ‘73, pages 73–118. North-Holland, 1975
• Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin Löf ’s Type Theory: An Introduction. Clarendon Press, Oxford, 1990
• Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002
• Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoret. Comput. Sci. Cambridge University Press, 1989
• Andreas Abel. Normalization by Evaluation: Dependent Types and Impredicativity. Unpublished, 2013. Habilitation thesis, Faculty for Mathematics, Informatics, and Statistics (MIST), Ludwig-Maximilians-University Munich
• Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In Proc. of the 22nd IEEE Symp. on Logic in Computer Science (LICS 2007), pages 3–12. IEEE Computer Soc. Press, 2007
• Andreas Abel and Gabriel Scherer. On irrelevance and algorithmic equality in predicative type theory. Logical Meth. in Comput. Sci., 8(1:29):1–36, 2012. TYPES’10 special issue

Oliver Kutz and Till Mossakowski

• Area: LoCo
• Level: I
• Week: 1
• Time: 11:00 – 12:30
• Room: D1.01

Abstract

There is a diversity of ontology languages in use, among them OWL, RDF, OBO, Common Logic, and F-logic. Related languages such as UML class diagrams, entityrelationship diagrams and object role modelling provide bridges from ontology modelling to applications, e.g. in software engineering and databases. Also in model-driven engineering, there is a diversity of diagrams: UML consists of 15 different diagram types, and SysML provides further types. Finally, in software and hardware specifcation, a variety of formalisms are in use, like Z, VDM, first-order logic, temporal logic etc.
Another diversity appears at the level of ontology, model and specification modularity and relations among ontologies, specifications and models. There is ontology matching and alignment, module extraction, interpolation, ontologies linked by bridges, interpretation and refinement, and combination of ontologies, models and specifications. The Distributed Ontology, Modeling and Specification Language (DOL) aims at providing a unified metalanguage for handling this diversity. In particular, DOL provides constructs for

• “as-is” use of ontologies, models and specifications (OMS) formulated (as a logical theory) in a specific ontology, modelling or specification language,
• OMS formalised in heterogeneous logics,
• modular OMS,
• mappings between OMS,
• networks of OMS, and
• queries.

The final DOL specification was submitted as a standard to the Object Management Group (OMG) in early 2015. This course will introduce syntax and semantics of the DOL language, discuss a number of modelling and interoperability problems that can be addressed with DOL, and introduce to the use of available DOL tools.

Slides

Day 1: Motivation and Introduction

Slides of Lecture 1 (PDF)

Day 2: Basic Structuring with DOL

Slides of Lecture 2 (PDF)

Day 3: Structured OMS

Slides of Lecture 3 (PDF)

Day 4: Semantics and Proof Calculus for Structured OMS

Slides of Lecture 4 (PDF)

Day 5: Advanced Concepts and Applications

Slides of Lecture 5 (PDF)

Additional References

Central page for DOL
Analysis and Proof Tool Hets, speaking DOL – please install Hets on your computer (Ubuntu). Fur Mac and Windows, use a virtual machine. If the local WLAN is too slow for that, see here. If you have downloaded a VM, please update to the latest Hets version as follows:
sudo apt-get update
sudo apt-get remove hets-core
sudo apt-get install hets-desktop-all

Hets for Mac:

brew tap spechub/hets
brew install hets-server
brew install hets-desktop

emacs mode for DOL

Ontohub web platform, speaking DOL – please create an account at Ontohub
DOL examples for ESSLLI

T. Mossakowski, M. Codescu, F. Neuhaus, O. Kutz
The Distributed Ontology, Modelling and Specification Language – DOL
The Road to Universal Logic, Festschrift for the 50th Birthday of Jean-Yves Béziau, Volume II, Editors: Arnold Koslow and Arthur Buchsbaum, Springer, 2015

PDF

 

Dmitry Chistikov and Rayna Dimitrova

• Area: LoCo
• Level: I
• Week: 1
• Time: 11:00 – 12:30
• Room: C2.06

Abstract

Model counting for logical theories, also known as #SMT,
generalizes such problems as counting the number of satisfying
assignments of Boolean formulae and computing the volume of
polytopes in a multi-dimensional space. These problems are
becoming more and more important in various application domains
(such as quantitative information flow and static analysis of
probabilistic programs).

This course is an introduction to #SMT and is built around measured
theories, a common logical framework for model counting problems.
We show that exact model counting, in contrast to satisfiability,
can be prohibitively hard.
For approximate model counting, we study Monte Carlo-based methods,
as well as hashing-based techniques that were originally developed
in the 1980s for #SAT in computational complexity theory.
We also show how combinations of different techniques make it possible
to address today’s challenges in model counting.

Tentative schedule

Monday: Introduction to model counting. Basics of logical theories, SAT, and SMT.

Tuesday: Model counting and computational complexity: P, NP, and #P.
Measures and probability theory; events, random variables, distributions.

Wednesday: Randomized algorithms. Monte Carlo methods for model counting
(over discrete and continuous domains), Markov chain Monte Carlo.

Thursday: Hashing-based approach to model counting over discrete domains.

Friday: From discrete to continuous model counting.

Slides

Monday
Tuesday
Wednesday
Thursday
Friday

Problem Sets

Monday(Corrected)
Tuesday
Wednesday and Thursday

Additional References

Sponsorship

This course is sponsored by

Uli Sattler and Thomas Schneider

• Area: LoCo
• Level: F
• Week: 1
• Time: 09:00 – 10:30
• Room: D1.03

Abstract

Description Logics (DLs) form the logical underpinning of state-of-the-art ontology languages such as OWL, and have a long history in knowledge representation. OWL is used to describe the meaning of terms used, e.g., in electronic health records, in a machine-processable way. In order to engineer large ontologies such as the NCI Thesaurus, suitable tool support is required, an interesting part of which is based on DL reasoning problems and the corresponding algorithms. Both classical reasoning problems – e.g., consistency and satisfiability – and more exotic reasoning problems – e.g., explanation and module extraction – play a central role, and are well-understood both in theory and in practice. We will introduce DLs and the role they play in OWL. Starting with a basic DL, ALC, we will

• discuss the relevant standard reasoning problems
• describe algorithms for these problems that perform very well in practice,
• outline the computational complexity of ALC and extensions,
• and review two non-standard reasoning services, namely those related to explanation and modularity.

Along the way we will connect the theoretical foundations with practical aspects by

• giving an overview of OWL and the ontology editor Protégé,
• reviewing applications from NLP,
• demonstrating how to use reasoners via the OWL API.

The course is on a foundational level and requires no previous knowledge (although familiarity with classical and/or modal logic would be an advantage).

Slides

• First Day:
  • Day 1: Intro (Part 1), also available with 4 per page
  • Day 1: Intro (Part 2), also available with 4 per page
  • The OWL ontology around Bodyparts and Diseases as used a running example
• Second Day:
  • Day 2: Relation with other logics, also available with 4 per page
  • Day2: ALC Tableau, also available with 4 per page
• Third Day:
  • Day3: Tableau (ctd), also available with  4 per page
  • Day 3: Complexity Intro, also available with 4 per page
• Fourth Day:
  • Day 4: Complexity, also available with 4 per page
  • Day4: Complexity & Undecidability    also available with 4 per page
• Fifth Day:
  • Day5: Complexity & Justifications, also available with 4 per page
  • Day5: Modularity & Overview, also available with 4 per page

The remaining slides will be made available during the week. Feel free to have a look at the material from previous versions of the course:

• at NASSLLI 2016
• at ESSLLI 2012

Additional References

For more information, have a look at

• proceedings of past Description Logic workshops
• proceedings of KR, Principles of Knowledge Representation and Reasoning
• The Description Logic Handbook, Cambridge University Press
• for stuff on OWL, visit
  • the official OWL site or
  • the new OWL community group or
  • our OWL in Manchester site
• Halpern and Moses’ “guide” paper on complexity (among others) of modal logics if you want to learn a little more about computational complexity.

To use the Protégé OWL editor, visit their web site and install Protégé Desktop (currently version 5). Feel free to send us an email if you have any questions!