19324417 Seminar / Undergraduate Course

WiSe 16/17: Seminar/Proseminar: Higher-Order Theorem Proving

Alexander Steen, Max Peter Wisniewski

Additional information / Pre-requisites

Additional Information:

The page of the event is available here

Comments

In this seminar, we discuss theoretical and practical aspects of interactive and automated theorem proving in classical higher-order logic (HOL). Theorem provers are computer programs that take a number of assumptions ("axioms") and a conjecture and then try to prove/refute that the conjecture is indeed a logical consequence of the given assumptions. Theorem provers can be employed in various disciplines of mathematics and computer science, e.g. for program verfication (prove that some assertion holds), for proof assistance (verify that my own proof is correct) and other fields of formal methods. Recent research also suggests that especially theorem provers for higher-order logic can be employed for verifying/analyzing arguments from theoretical philosophy/metaphysics.

What are the mathematical foundations for such programs? How can they be implemented (efficiently)? Many of the discussed topics are currently of research interest and can lead to ambitious bachelor's and master's theses.

Possible topics include:

  • Simply typed lambda calculus, theoretical properties, examples;
  • Introduction into higher-order logic, history, syntax, semantics;
  • Proof calculi, Automation, Soundness and Completeness;
  • Cut-Elimination, Cut-Simulation;
  • Unification, Pre-Unification;
  • Skolemization, Normal forms;
  • Transformations into first-order logic;
  • Implementation techniques (Indexing, selection heuristics, ...)
and more

close

Suggested reading

Literature:

Will be announced on the events page.

16 Class schedule

Additional appointments

Thu, 2016-10-06 14:00 - 16:00
Vorbesprechung

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Regular appointments

Thu, 2016-10-20 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2016-10-27 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2016-11-03 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2016-11-10 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2016-11-17 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2016-11-24 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2016-12-01 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2016-12-08 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2016-12-15 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2017-01-05 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2017-01-12 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2017-01-19 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2017-01-26 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2017-02-02 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2017-02-09 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Thu, 2017-02-16 14:00 - 16:00

Lecturers:
Max Peter Wisniewski
Alexander Steen

Location:
T9/051 Seminarraum (Takustr. 9)

Subjects A - Z