| | 9 |
: | 00 |
- | 10 |
: | 00 |
Invited Talk: Algorithms and Data
Structures for First-Order Equational Deduction |
| | |
Stephan Schulz |
|
| | 10 |
: | 00 |
- | 10 |
: | 30 |
Coffee Break |
|
| | 10 |
: | 30 |
- | 11 |
: | 00 |
Term Indexing for the LEO-II Prover |
| | |
Frank Theiss and Christoph Benzmüller |
| | 11 |
: | 00 |
- | 11 |
: | 30 |
Integrating External Deduction Tools with ACL2 |
| | |
Matt Kaufmann, J Strother Moore,
Sandip Ray, and Erik Reeber |
| | 11 |
: | 30 |
- | 12 |
: | 00 |
Efficiently Checking Propositional Resolution
Proofs in Isabelle/HOL |
| | |
Tjark Weber |
|
| | 12 |
: | 00 |
- | 14 |
: | 00 |
Lunch |
|
| | 14 |
: | 00 |
- | 15 |
: | 00 |
Invited Talk: Implementing an
Instantiation-based Theorem Prover for First-order Logic |
| | |
Konstantin Korovin |
|
| | 15 |
: | 00 |
- | 15 |
: | 30 |
Coffee Break |
|
| | 15 |
: | 30 |
- | 16 |
: | 00 |
Tableau Decision Procedure for Propositional
Intuitionistic Logic |
| | |
Guido Fiorino, Alessandro Avellone, and
Ugo Moscato |
| | 16 |
: | 00 |
- | 16 |
: | 30 |
Combining First-Order State Abstraction with
Heuristic Search in a Logic-Based Planning System |
| | |
Olga Skvortsova, Steffen Hölldobler,
and Eldar Karabaev |
| | 16 |
: | 30 |
- | 17 |
: | 00 |
Multiple Preprocessing for Systematic SAT
Solvers |
| | |
Anbulagan A. and John Slaney |
|
| | 17 |
: | 00 |
- | 18 |
: | 00 |
Panel Interrogation |
| | |
A panel of experts on the implementation of
logics will answer questions collected from the workshop
attendees. |