 | Towards Practice-Oriented Formal Reasoning Using Three-Valued Logic
Antti Valmari and Mika Hirvensalo
The goal of this paper is to lay the foundation for versatile practical formal reasoning in the presence of undefined terms, at the level of first-year university mathematics courses.
In earlier research, a tool has been developed for checking reasoning about real numbers or integers, using first-order formulas with ``almost linear''terms.
It was based on decision and counter-example generation algorithms, and thus did not require the user to justify reasoning steps.
The new approach relies on the user providing justification of the kind suitable for humans, so that much more general problems than ``almost linear'' could be dealt with.
A main purpose of the work is to support teaching and learning the logical principles underlying mathematical proofs.
There is not yet any tool implementing the new ideas, but a fully formal manual example of a challenging proof using them is presented.
July 2026
|
Back
