登入選單
返回Google圖書搜尋
Logical Environments
註釋Logical environments are computer systems that provide engineers and mathematicians with facilities to develop formal proofs. They also give some reasoning assistance and manage a data base of axiomatisations and theorems. Applications include both software and hardware certification. The design of such environments is an active research topic, at the frontier between mathematical logic and software engineering. Research ranges from abstract speculations about the foundations of mathematics, to very concrete considerations about ergonomic tools for building user interfaces with current workstation technology. New ideas in Type Theory may be put to use in a new generation of proof assistants taking advantage of uniform structures for the representation of mathematical and logical data. European Computer Science is specially active in this promising area, whose progress is crucial for safety-critical computer applications. The present volume is a selection of papers from research centres in Europe and the USA; together they give an overview of recent progress in the area.