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, ...)
Suggested reading
Literature:
Will be announced on the events page.
16 Class schedule
Additional appointments
Thu, 2016-10-06 14:00 - 16:00Regular appointments