# 185.A60 Higher-order Logic Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_21",{id:"j_id_21",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_23",{id:"j_id_23",showEffect:"fade",hideEffect:"fade",target:"isAnySteop"});}); 2019S 2017S 2016S 2014S 2013S 2012S

2019S, VU, 2.0h, 3.0EC

## Merkmale

• Semesterwochenstunden: 2.0
• ECTS: 3.0
• Typ: VU Vorlesung mit Übung

## Ziele der Lehrveranstaltung

A formal introduction to strong logical formalisms, demonstrating their varying expressivity and limitations by establishing their properties via proof; also touching on the application of these formalisms in modeling and specification in computer science.

## Inhalt der Lehrveranstaltung

Limits of first-order definability, syntax and semantics of second-order logic, expressive power of second-order logic, second-order arithmetic, simple type theory, typed lambda calculi, higher-order logic, Henkin semantics, interactive theorem proving in higher-order logic

## Weitere Informationen

First meeting: Tuesday, 7 May 2019, 15:00, seminar room "Gödel".

## Vortragende Personen

• Ramanayake, Don Revantha Shiyan

## Leistungsnachweis

Three assignments

## LVA-Anmeldung

Von Bis Abmeldung bis
13.12.2018 00:00 01.07.2019 23:00

## Curricula

StudienkennzahlVerbindlichkeitSemesterAnm.Bed.Info
066 931 Logic and Computation Gebundenes Wahlfach

## Literatur

- Stefan Hetzl: Higher-order logic. Lecture notes.*main reference*

- Stefan Hetzl: Mathematical Logic 2. Lecture notes.*Prerequisite material on first-order logic*

- Johan Van Benthem and Kees Doets. Higher-order logic. Book chapter. Handbook of Philosophical Logic. Vol. 164, pages 275-329.*

- Daniel Leivant: Higher-order Logic, Handbook of Logic in Artificial Intelligence and Logic Programming (2) 1994, pages 229-322.*

- Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, Academic Press, 1986

- Dale Miller and Gopalan Nadathur: Programming with Higher-Order Logic, Cambridge University Press, 2012

- Chad E. Brown: Automated Reasoning in Higher-Order Logic, College Publications, 2007

- Henk Barendregt, Wil Dekkers and Richard Statman: Lambda Calculus with Types, 2013

-  Manzano: Extensions of first-order logic, 1996.

-  M.H. Sorensen and P. Urzyczyn: Lectures on the Curry-Howard Isomorphism, 2006

## Vorkenntnisse

This is an advanced course in logic. Firm knowledge of classical first-order logic (formulas, models, proofs) is a prerequisite. In the first couple of lecture I will overview the key definitions and results from first-order logic.

Englisch