Algebraic Specification and Verification – an Introduction to CafeOBJ

Norbert Preining

  • Area: LoCo
  • Level: I
  • Week: 2
  • Time: 09:00 – 10:30
  • Room: C3.06 A5.18

Abstract

Ensuring correctness of complex systems like computer programs or communication protocols is gaining ever increasing importance. For correctness it does not suffice to consider the finished system, but correctness already on the level of specification is necessary, that is, before the actual implementation starts. To this aim, algebraic specification and verification languages have been conceived. They are aiming at a mathematically correct description of the properties and behavior of the systems under discussion, and in addition often allow to prove (verify) correctness within the same system.

This course will give an introduction to algebraic specification, its history, logic roots, and actuality with respect to current developments. Paired with the theoretical background we give an introduction to CafeOBJ, a programming language that allows both specification and verification to be carried out together. The course should enable students to understand the theoretical background of algebraic specification, as well as enable them to read and write basic specifications in CafeOBJ.

Description

CafeOBJ is a specification language based on three-way extensions to many-sorted equational logic: the underlying logic is order-sorted, not just many-sorted; it admits unidirectional transitions, as well as equations; it also accommodates hidden sorts, on top of ordinary, visible sorts. A subset of CafeOBJ is executable, where the operational semantics is given by a conditional order-sorted term rewriting system.

The language system CafeOBJ has been under constant development at the institute of the lecturers since the late 80ies. It is closely related to other algebraic specification languages in the OBJ family, including Maude. The CafeOBJ language and the range of verification methods and tools it supports – including its support for inductive theorem proving, verification of behavioral specifications, deductive invariant proof, and reachability analysis of concurrent systems – has played a key role in both extending and bringing algebraic specification techniques into contact with many software engineering applications.

The following topics will be discussed:

  • algebraic foundations: many-sorted algebras, order-sorted algebras, behavioral specification
  • computational foundations: rewriting
  • programming with CafeOBJ: language elements, modules, simple programs
  • CloudSync: presentation of an example cloud synchronization protocol and its verification

To make the lectures not too `heavy’, we will structure each lecture into two parts: A first part providing an introduction of some theoretical concept, or framework, and a second part dealing with actual programming and implementation. Especially for the second part of each lecture students are encouraged to use their laptops to try out code and experiment.

In addition, if time permits, we are willing to provide out-of-lecture lab-style meeting where we help students to get CafeOBJ installed and running, as well as making the first steps.

Code

Code used during the lessons and solutions to the exercises

  • Day 1 and Day 2: cafe.zip
  • Emacs initialization file: dot.emacs – save as .emacs in your home directory
  • Updated cloudsync file for current CafeOBJ interpreter: cloudsync-20160824.cafe (rename the file to cloudsync-20160824.cafe)
  • Day 4: cafe4.zip

Slides

Additional References


Introduction to Non-Monotonic Logic

Mathieu Beirlaen and Christian Strasser

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

Abstract

Informally, a logic is non-monotonic if under the addition of new premises we may lose some consequences which were previously derivable. This means that some of our inferences are defeasible: in view of additional information they may get retracted. Examples of defeasible reasoning patterns are numerous: induction, inference to the best explanation, inferences on the basis of expert opinions, reasoning in the presence of inconsistencies, reasoning with priorities, etc. In our everyday practice as well as in the practice of experts (e.g. medical diagnosis) or scientists, defeasible inferences are abundant.

In this course, we present, discuss, and compare some of the principal formalisms for representing defeasible inferences via non-monotonic logics. We introduce the framework of inheritance networks, Reiter’s default logic, argumentation frameworks, preferential semantics, and adaptive logics. Each of these frameworks is representative of a large research tradition within the field of non-monotonic logic. In our course the interested student gets equipped with a basic understanding that will enable her to dig deeper into the literature and to understand similar techniques in formalisms that are not covered in the course.

Slides

Slides day 1 (preferred models)

Slides day 2 (adaptive logics)

Slides day 3 (maximal consistent subsets)

Slides day 4 (default logic)

Slides day 5, part 1 (abstract argumentation)

Slides day 5, part 2 (structured argumentation)

Additional References

Bibliography (days 1 and 2)


Deontic modality: Linguistic and Logical Perspectives on Oughts and Ends

Cleo Condoravdi and Leendert van der Torre

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

Abstract

The aim of the course is to enable dialogue between practitioners of logical and linguistic approaches to deontic modality. We examine the semantics of conditional ought broadly construed, including normative, teleological, bouletic, deliberative and advice modals. We present the basic issues raised by modalities and the principal linguistic and logical approaches to them, highlighting their conceptual similarities and differences. Each day of the course presents a new development in deontic logic that features in current debates: practical reasoning (such as means-end reasoning), norm and obligation dynamics, detachment, and multi-agent interaction (as used to model advice uses). All these four challenges are illustrated and analyzed as part of an in-depth discussion of a single problem: the formalization of anankastic conditionals.

  1. Monday: History of deontic logic as a debate between classical vs. alternative semantics. Anankastic conditionals as a central challenge for deontic reasoning.
  2. Tuesday: Kratzer framework for natural language modality, and its relation to Poole default logic. Practical reasoning, in particular means-end reasoning.
  3. Wednesday: Norm change. The AGM framework of theory change. Anankastics as norm change in the Kratzer framework.
  4. Thursday: Endorsement, conditional imperatives, objective versus subjective oughts.
  5. Friday: Pragmatics, advice and other scenarios. Wrap up and outlook.

Slides and handouts

Lecture 1 DSDL

Lecture 1 intro anankastics

Lecture 2 Kratzer means-end

Lecture 2 Poole

Additional References

  1. H. Prakken, M. Sergot 1996: Contrary-to-Duty Obligations. Studia Logica 57(1): 91-115.
  2. K.J. Sæbø 2001: Necessary conditions in a natural language. In: Audiatur Vox Sapientiae: A Festschrift for Arnim von Stechow. Akademie-Verlag, 427–449.
  3. A. Kratzer 1981. The notional category of modality. In: Words, worlds and contexts. De Gruyter, 38-74.
  4. D. Poole 1988. A Logical Framework for Default Reasoning. Artif. Intell. 36(1): 27-47
  5. S. O. Hansson 1993. Reversing the Levi identity. J. Philosophical Logic 22(6): 637-669.
  6. A. von Stechow, S. Krasikova and D. Penka. 2006. Anankastic conditionals again. In A Festschrift for Kjell Johan Sæbø. Forfatterne, 151–171.
  7. C. Condoravdi and S. Lauer. 2016. Anankastic conditionals are just conditionals. Semantics and Pragmatics 9(8).

Composition in Probabilistic Language Understanding

Gregory Scontras

  • Area: LaLo
  • Level: A
  • Week: 2
  • Time: 09:00 – 10:30
  • Room: D1.03
  • Course website

Abstract

Recent advances in computational cognitive science (i.e., simulation-based probabilistic programs) have paved the way for significant progress in formal, implementable models of pragmatics. Rather than describing a pragmatic reasoning process, these models articulate and implement one, deriving both qualitative and quantitative predictions of human behavior—predictions that consistently prove correct, demonstrating the viability and value of the framework. However, these models operate at the utterance level, taking as their starting point whatever the compositional semantics delivers to them as the meaning of a proposition; the models deliberately avoid the composition of the literal interpretations over which they operate. We aim to change that, further shrinking the theoretical and practical distance between semantics and pragmatics by incorporating both within a single model of meaning in language. To that end, this course examines the ways that a semantic compositional mechanism may be modeled dynamically and probabilistically, within the broader framework of computational cognitive science.


Formal Semantics of Natural Language

Yoad Winter

  • Area: LaLo
  • Level: F
  • Week: 2
  • Time: 09:00 – 10:30
  • Room: D1.02

Abstract

The course will give a concise introduction to compositional modeltheoretic semantics in the Montague tradition, with new directions coming from recent research. Concentrating on the underlying methodological principles, I will aim to attract students’ attention to the scientific value of describing intricate semantic phenomena using elegant and rigorously-defined mathematical techniques. The course is intended for students who don’t necessarily have deep knowledge in logic or linguistics, but have basic mathematical or general scientific background. The foundational material includes: entailment, ambiguity, compositionality, direct interpretation, types and model structure, boolean operators, generalized quantifiers and abstract categorial grammar. Motivations and examples will draw on recent research of coordination, quantifier scope, spatial expressions, and long-distance dependencies. Further remarks about diverse problems involving plurality, intensionality, concepts in language, and experimental pragmatics/semantics will be made as time permits.

At the end of the course, students will have acquired basic formal notions of natural language semantics, which will allow them to approach much of the literature in this field.

The course is based on the textbook Elements of Formal Semantics, which will appear in 2016. It follows courses that I have taught at ESSLLI 2013 and NASSLLI 2014.

 

Slides — http://www.phil.uu.nl/~yoad/tmp/slides-Winter-ESSLLI2016.pdf


A Journey through the Possible Worlds of Modal Logic

Valentin Goranko

  • Area: LaLo
  • Level: F
  • Week: 2
  • Time: 11:00 – 12:30
  • Room: D1.01

Abstract:

This course will introduce some of the most popular families of modal logics: alethic, epistemic, doxastic, temporal, deontic, and agentive. I will discuss their philosophical motivations, will present the basic technical background of possible worlds semantics and illustrate its use for modelling and reasoning about various philosophical issues. The emphasis will be on conceptual understanding and thought provocation rather than technical detail and depth. The course is intended for a broad audience with some background on classical logic and general appreciation of philosophical aspects of logic.

Slides

will be added during the course on this course webpage.

Additional References

Visit the course webpage


Genericity in Natural Language

E. Graham Katz and Roberto Zamparelli

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

Abstract

The phenomenon of genericity is pervasive in natural language, and it has been addressed by a huge body of literature in natural language semantics, starting from the seminal work of (Lawler, 1973) and (Carlson, 1977) and continuing to the present.
The goal of the course proposed here is to offer a historical review of the main approaches to nominal and sentential genericity, but also cover some recent developments, in particular the relation between kinds and psychological concepts, the more recent implementations of genericity within in the syntax/semantics interface, and the possibility to build theoretical, probability-based analysis of this phenomenon, but also computational distributional models of genericity, with the aim of accounting for human intuitions about the truth or falsity of these expressions.

Slides

Additional References

  • Carlson, G. (1977). Reference to Kinds in English. PhD thesis, University of Massachusetts at Amherst.
  • Lawler, J. (1973). Studies in English Generics. University of Michigan Papers in Linguistics,

Notes (updates as the course progresses)


The Role of Linguistic Interpretation in Human Failures of Reasoning

Salvador Mascarenhas

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

Abstract

Research in linguistic semantics and in the psychology of reasoning overlaps significantly. Both fields study the nature of mental representations of sentences, as well as the ways in which sentences are related to form entailment patterns. Linguistic semantics has produced sophisticated models of sentence interpretation, while the psychology of reasoning has catalogued and analyzed many of the ways in which human inference making diverges from what is logically sanctioned. But the two fields have progressed in parallel, with little interaction. Consequently, some if not many of the fallacies studied in psychology can in principle have been misdiagnosed as failures of reasoning, when in fact they are the result of sound reasoning acting on non-obvious but legitimate interpretations of the premises. This course explores the gap between semantics and reasoning, contrasting competing accounts in the realms of reasoning with disjunctions, conditionals, and probabilities.

Handouts

Lecture 1 handout

Lectures 2 and 3 handout (updated: simplified formal definitions of ETR operations now have informal glosses in English)

Lecture 4 handout

Additional References


Executable Semantic Parsing

Jonathan Berant

  • Area: LaCo
  • Level: A
  • Week: 2
  • Time: 09:00 – 10:30 (we start on time!)
  • Room: C2.06

News

  • Thanks for attending the class! Don’t forget to give me feedback!
  • Give me feedback! Answer some simple questions here after tomorrow’s class.
  • What will we do tomorrow? You decide! Fill out this survey.
  • I didn’t get to talk about cube pruning for K-best parsing, but put a link to a presentation on the topic below.
  • If you missed class and would like to catch up one good way of doing that (other than going through the slides) is to go over the Sempre tutorial.
  • I added grammar and lexicon files for exercises and examples in class 3.
  • I updated the slides for class 1 to include the solution for the exercise + some type corrections.
  • To have better editting of your sempre commands install rlwrap.

Abstract

Executable semantic parsing is the task of mapping natural language utterances into meaning representations that can be executed against a background knowledge-base. Interest in executable semantic parsers has raised dramatically in the past few years, as conversational interfaces are becoming more and more ubiquitous. The goal of this class is to provide an introduction to executable semantic parsing and to highlight the challenges in scaling semantic parsers to large domains. We will focus on three main questions: (a) What are the formal representations for natural language and how can one bridge the gap between natural language and formal language. (b) How can we learn to translate from natural language to formal language without requiring annotations of the formal language. (c) How can we develop algorithms that search through the space of logical forms efficiently.

Exercises

Classes will include hands-on sections in which students will use the SEMPRE package to practice the material taught in class. ESSLLI will provide a virtual machine that students can connect to with SEMPRE already installed. However, it is easy and recommended to install SEMPRE on your own laptop if you have one by following these steps:

  1. Install all requirements as described in the installation section of SEMPRE.
  2. Install rlwrap (not required but makes life a lot easier).
  3. Install SEMPRE:

git clone https://github.com/percyliang/sempre
cd sempre

Download external dependencies (this might take a few minutes):

./pull-dependencies core corenlp esslli_2016 tables

Create a symbolic link for easier access later on:

ln -s lib/data/esslli_2016/esslli_2016 esslli_2016

Compile:

ant core corenlp tables

Now test by running:

./run @mode=simple-lambdadcs

You will see a prompt. Use the following command to load a database:

(loadgraph esslli_2016/geo880.kg)

To verify you uploaded the database type:

(context)

You will see a lot of text. Now try to issue a simple query:

(execute mountain.maroon)

If SEMPRE returns a list containing mountain.marron you succeeded and you are done! To exit type ctrl+D

Compliation problem

If you get a compilation error complaining about the “Pair” class among other things do the following:

ant clean
rm -rf fig
./pull-dependencies core
ant core corenlp tables

Tentative Schedule

Class 1: slides

  • Introduction
  • Representations
    • Lambda calculus
    • Lambda-DCS

SHRDLU

Class 2: slides

  • Compositionality
    • Grammars
    • Lexicons
    • Derivations

simple grammar
simple lexicon

Suggested solution for exercise 2. Try to use it only when stuck…
ex2 grammar
ex2 lexicon

Class 3: slides

  • Learning

Example grammar
Example lexicon

Class 4:
slides

  • Parsing algorithms
    • CKY
    • Coarse parsing
    • Agenda-based parsing

k-best parsing

Class 5:

  • Advanced topics
    • Intermediate representations
    • Building a parser overnight
    • Deep learning

Additional References

Past tutorial on semantic parsing (focused on CCG and SPF)

High level overview of statistical semantic parsing


Modelling Dialogue: Building Highly Responsive Conversational Agents

Stefan Kopp and David Schlangen

  • Area: LaCo
  • Level: A
  • Week: 2
  • Time: 09:00 – 10:30
  • Room: C2.01 C3.06

Abstract

Formal semantics and pragmatics, if it goes beyond single speech acts at all, typically starts from an idealised view of dialogue as the exchange of propositions, one coming after another. In reality, dialogue is a much more dynamic and rich activity: people ‘um’ and ‘ah’, finish each other’s utterances, laugh, and gesture, and they engage in dialogue not only (and often, not even predominantly) to exchange information, but to bond and enjoy themselves. For different, but converging reasons, technical systems also try to abstract away from this dynamic and multimodal nature of dialogue. In this course, we will look into the phenomenology of dialogue, and specifically into its nature as something that is co­-constructed and improvised by its participants. We will use computational modelling to gain insights into these phenomena, and also into the perspectives for realising more natural interaction with technical systems.

Slides / Information

Additional References