Talk:Automated Assistance for Formal Reasoning
From Automated Assistance for Formal Reasoning
Many systems are claimed to be "human-friendly", "human-accessible", or "human-readable" [1]. However, no clear definition or measure of this characteristic is provided.
Contents |
References
[1] M. Wenzel. Isabelle/Isar - a versatile environment for human-readable formal proof documents. Technische Universität München.
The eventual goal of this interface is to support semantic machine comprehension of formal reasoning as it is practiced by human users.
Benefits
- Verification is a subset of corroboration: scalable and broadly relevant corroboration capabilities can be turned into scalable and broadly applicable verification capabilities.
- Consequences for interfaces, error message composition.
- We try to couple users directly with a basic verifier, and this isn't practical for many users. By introducing a comprehensive context, we provide a new target for verification efforts: not the users themselves (possibly guided by some relatively restrictive interactive protocol) but the comprehensive context (that is, the "trace" of the comprehensive context). There is no need to try to verify an interaction with a user: export the interface and comprehension problem to someone else (the abstraction), and worry about verifying that intermediate representation.
There is, at this point, no explicit focus on an intermediate representation in verification efforts. The repository and natural context is a target for those interested in total verification: find a way to verify the library. Bold text
Old text
This system demonstrates the benefits of creating appropriate interfaces, suitable normalized representations, and parallelizable search heuristics for formal reasoning and automated verification tools. The design of the verifier and its underlying logic are meant to be simple, straightforward, and flexible.
