Three-valued logic and Isabelle: the problems

Dirk Van Heule

ABSTRACT

Using the prooftool Isabelle is one thing, implementing a new object-logic for it is two however.

In this talk we will focus on the problems and the solutions we encountered when building the Partial Predicate Calculus as an object-logic for Isabelle.

Items such as three-valued logic, syntax vs. semantics, hypsubstfun, quantifiers, classical reasoner and sequents will be discussed.