LEGO is a powerful tool for interactive proof development in the natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs. For example, the features of the system like argument synthesis and universe polymorphism make proof checking more practical by bringing the level of formalization closer to that of informal mathematics. The higher-order power of its underlying type theories, plus the support of specifying new inductive types, provides an expressive language for formalization of mathematical problems and program specification and development. Particularly, the type universes in the type theory make it possible to formalize abstract mathematics, and the strong sum types (Sigma-types) can be used to naturally express abstract structures, mathematical theories and program specifications. LEGO may also be used to formalize different logical systems and prove theorems based on the defined logics.
References:
http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-211/
ليست هناك تعليقات:
إرسال تعليق