CADE-14 Papers
| Session 1: Invited Lecture | Chair: William McCune | |
|---|---|---|
| 9:00-10:00 | Professor Wu Wen-Tsün, Academia Sinica, Beijing, China | |
| 10:00-10:30 | Break | |
| Session 2 | Chair: Deepak Kapur | |
| 10:30-11:00 |
Decidable Call by Need Computations in Term Rewriting Irène Durand, Aart Middeldorp | |
| 11:00-11:30 |
A New Approach for Combining Decision Procedures for the Word Problem,
and Its Connection to the Nelson-Oppen Combination Method Franz Baader, Cesare Tinelli | |
| 11:30-12:00 |
On Equality Up-to Constraints over Finite Trees, Context Unification
and One-Step Rewriting Joachim Niehren, Manfred Pinkal, Peter Ruhrberg | |
| 12:00-2:00 | Lunch | |
| Session 3: System Descriptions | Chair: Geoff Sutcliffe | |
| 2:00-2:15 |
Dedam: A Kernel of Data Structures and Algorithms for Automated
Deduction with Equality Clauses Robert Nieuwenhuis, José Miguel Rivero, Miguel Angel Vallejo | |
| 2:15-2:30 |
The Clause-Diffusion Theorem Prover Peers-mcd Maria Paola Bonacina | |
| 2:30-2:45 |
Integration of Automated and Interactive Theorem Proving in ILF Bernd Ingo Dahn, Jürgen Gehne, Thomas Honigmann, Andreas Wolf | |
| 2:45-3:00 |
ILF-SETHEO: Processing Model Elimination Proofs for Natural Language
Output Andreas Wolf, Johann Schumann | |
| 3:00-3:15 |
SETHEO Goes Software Engineering: Application of ATP to Software
Reuse Bernd Fischer, Johann Schumann | |
| 3:15-3:30 |
Proving System Correctness with KIV 3.0 Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel | |
| 3:30-4:00 | Break | |
| Session 4 | Chair: Jieh Hsiang | |
| 4:00-4:30 |
A Practical Symbolic Algorithm for the Inverse Kinematics of 6R
Manipulators with Simple Geometry Lu Yang, Hongguang Fu, Zhenbing Zeng | |
| 4:30-5:00 |
Automatic Verification of Cryptographic Protocols with SETHEO Johann Schumann | |
| 5:00-5:30 |
A Practical Integration of First-Order Reasoning and Decision
Procedures Nikolaj S. Bjørner, Mark E. Stickel and Tomás E. Uribe | |
Tuesday 15th July
Session 5
Chair: Hantao Zhang
9:00-9:30
Some Pitfalls of LK-to-LJ Transformations and
How to Avoid Them
Uwe Egly
9:30-10:00
Deciding Intuitionistic Propositional Logic via Translation into
Classical Logic
Daniel Korn, Christoph Kreitz
10:00-10:30
Break
Session 6
Chair: Johann Schumann
10:30-11:00
Lemma Matching for a PTTP-based Top-down Theorem Prover
Koji Iwanuma
11:00-11:30
Exact Knowledge Compilation in Predicate Calculus: the Partial
Achievement Case
Olivier Roussel, Philippe Mathieu
11:30-12:00
Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up
Theorem Proving
Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta and Miyuki
Koshimura
12:00-2:00
Lunch
Free time
Wednesday 16th July
Session 7: Invited Lecture
Chair: William McCune
9:00-10:00
Professor Moshe Vardi, Rice University, Houston, Texas, USA
10:00-10:30
Break
Session 8
Chair: Andrei Voronkov
10:30-11:00
Connection-Based Proof Construction in Linear Logic
Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt
11:00-11:30
Resource-distribution via Boolean Constraints
James Harland, David Pym
11:30-12:00
Constructing a Normal Form for Property Theory
Mary Cryan, Allan Ramsay
12:00-2:00
Lunch
Session 9: System Descriptions
Chair: Harald Ganzinger
2:00-2:15
OMEGA: Towards a Mathematical Assistant
Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer,
Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase,
Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt,
Jörg Siekmann, Volker Sorge
2:15-2:30
PLAGIATOR: A Learning Prover
Thomas Kolbe, Jürgen Brauburger
2:30-2:45
CODE: A Powerful Prover for Problems of Condensed Detachment
Dirk Fuchs, Matthias Fuchs
2:45-3:00
A New Method for Testing Decision Procedures in Modal Logics
Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani
3:00-3:15
MINLOG: A Minimal Logic Theorem Prover
John Slaney
3:15-3:30
SATO: An Efficient Propositional Prover
Hantao Zhang
3:30-4:00
Break
Session 10
Chair: David McAllester
4:00-4:30
Using a Generalisation Critic to Find Bisimulations for Coinductive
Proofs
Louise Dennis, Alan Bundy, Ian Green
4:30-5:00
A Colored Version of the lambda-Calculus
Dieter Hutter, Michael Kohlhase
5:00-5:30
A Practical Implementation of Simple Consequence Relations Using
Inductive Definitions
Seán Matthews
Thursday 17th July
Session 11
Chair: Mark Stickel
9:00-9:30
Soft Typing for Ordered Resolution
Harald Ganzinger, Christoph Meyer, Christoph Weidenbach
9:30-10:00
A Classification of Non-Liftable Orders for Resolution
Hans de Nivelle
10:00-10:30
Break
Session 12
Chair: Ursula Martin
10:30-11:00
Hybrid Interactive Theorem Proving using Nuprl and HOL
Amy P. Felty, Douglas J. Howe
11:00-11:30
Proof Tactics for a Theory of State Machines in a Graphical
Environment
Katherine A. Eastaughffe, Maris A. Ozols, Tony Cant
11:30-12:00
RALL: Machine-supported Proofs for Relation Algebra
David von Oheimb and Thomas F. Gritzner
12:00-2:00
Lunch
Session 13: System Descriptions
Chair: John Slaney
2:00-2:15
Nuprl-Light: An Implementation Framework for Higher-Order Logics
Jason J. Hickey
2:15-2:30
XIsabelle
Maris A. Ozols, Tony Cant, Katherine A. Eastaughffe
2:30-2:45
XBarnacle: Making Theorem Provers More Accessible
Helen Lowe, David Duncan
2:45-3:00
The Tableau Browser Snarks
Mathias Kettner, Norbert Eisinger
3:00-3:15
Jape: A Calculator for Animating Proof-on-paper
Richard Bornat, Bernard Sufrin
3:15-3:30
CASC-14 and CISC-14 Reports
Christian Suttner, Geoff Sutcliffe, David McAllester
3:30-4:00
Break
Session 14
Chair: Claude Kirchner
4:00-4:30
Evolving Combinators
Matthias Fuchs
4:30-5:00
Partial Matching for Analogy Discovery in Proofs and
Counter-examples
Gilles Défourneaux, Nicolas Peltier
5:00-5:30
DiaLog: A System for Dialogue Logic
Jürgen Ehrensberger, Claus Zinn