Integrating Logic with Partial Functions into a Proof Checker
In 2010-2013 I developed a 3-valued logic for Partial Functions.
During 2013-2014, I tried to integrate this logic into an
interactive proof checker. It was unsuccesful.
(The resulting proof checker was too unpleasant to use.)
In this talk, I summarize a new attempt, which has not been implemented
yet:
- I explain basics of the underlaying 3-valued logic.
- How to generalize this logic to higher-order.
- How to build theories (using little theory). Theories can
be substantive or adjective in nature.
- Type Reductions. Explicit type conditions are useful, but very
unpleasant in practical use.