Abstract:
An operational model for intuitive proofs is suggested. It is a sequence of instructions. Operands of an instruction are formalized mathematical propositions. The set of instructions is extendable one. Operational semantics of instructions is defined by means of the macrolanguage based on the fixed set of basic operations. The residual model (macroexpansion) of the operational model for an intuitive proof which is formed by a macrogenerator is a program for a virtual machine. The successful completion of this program execution verifies correctness of the intuitive proof.
Keywords:intuitive proof, formalizing, operational model, macrolanguage, interactive system for theorem proving, automatic theorem proving, checking correctness of intuitive proofs.
Fulltext:
PDF file (542 kB)