Formal reasoning interface
From Automated Assistance for Formal Reasoning
The aartifact automated assistant is generated in an automated manner from a rich static context of common mathematical knowledge dealing with particular domains. Together, the aartifact system and the static context constitute a sophisticated interface and abstraction layer for formal reasoning tools.
Formal reasoning validation and verification systems are often designed as monolithic applications that encompass both the interface and verification procedures. We advocate a design for formal reasoning systems in which the interface and verification procedures are separated from one another, and in which it is the responsibility of the interface component to provide the bulk of a formal reasoning system's automation and comprehension capabilities. In this way, the interface component acts as a rich and complex abstraction layer that invokes more simple verification procedures. Furthermore, the interface component need not (and should not) ensure consistency; its purpose is only to ascertain and comprehend the intent of the user.
Such an interface encompasses many common components of formal reasoning systems, and we focus on four common components:
- syntax and parsers;
- interactive protocols;
- inference, search, and automation procedures;
- library of concepts, definitions, propositions, and results.
[edit] Inference, search, and automation procedures
The logical inference and search capabilities of the aartifact system are intentionally simple. A logic definition of the basic underlying logical inference rules is available.
