Ebook: Many-valued Logic in HOL

Internet-Publication. — 15 p. (pp.: 113-127). English.Abstract.
Many-valued logic is formalized in the logic of the theorem prover HOL [GM93]. We follow an algebraic approach, starting from a Heyting algebra. Using this approach and some useful HOL machinery, we implemented a tautology-checker for a three-valued propositional logic.Introduction.
Currently, a new specification language is under construction at the department of Computing Science in Groningen, called Almost Formal Specification Language, AFSL [Saa]. The semantics of AFSL is based on a three-valued logic. 1 We want to provide users of AFSL with a proper 'specification environment', analogous to a 'programming environment'. Since logic plays an important role in AFSL, a theorem prover might be the right medium to test different forms of toolsupport for the language. A theorem prover is to assist the process of making valid proofs. Therefore, each theorem prover has a proof system or logic in which the theorems are proven. This implies that all proofs we want to make with the prove...Introduction.
HOL.
Starting Point: a Heyting Algebra.
Tactics for Proof Support.
Rewriting.
Smart Tactics.
Induction.
General comments.
Example: A Tautology Checker for Three Valued Propositional Logic.
The Tactic.
Conclusions and Future Work.
Acknowledgements.
Appendix:
- Tacticals.
- Tactics.
- Theorem generators.
- ML-functions.
References.