TY - GEN

T1 - Computer aided reasoning

AU - Trybulec, Andrzej

AU - Blair, Howard A.

PY - 1985/1/1

Y1 - 1985/1/1

N2 - We present a language intended to be a first step in approximating the language of mathematical papers, and a validator; that is, a program that checks the validity of arguments written in this language. The validator approximates the activity of a mathematician in certifying the structure and correctness of the mathematical argument. Both components together constitute a computer aided reasoning (CAR) system. Versions of the system, called MIZAR, have been in use for a decade for discrete mathematics instruction. We are concerned here with the features of the MIZAR language that that are used to diminish the gap between formal natural deduction and mathematical vernacular. The inference checking component of the validator can be easily changed. We demonstrate the influence on the way the expressive power of the language can be exploited by contrasting, for a fixed proposition, two proofs embodying the same idea but for which different checking modules have been used. The more powerful inference checker that we discuss incorporates the formalization of obviousness given by M. Davis.

AB - We present a language intended to be a first step in approximating the language of mathematical papers, and a validator; that is, a program that checks the validity of arguments written in this language. The validator approximates the activity of a mathematician in certifying the structure and correctness of the mathematical argument. Both components together constitute a computer aided reasoning (CAR) system. Versions of the system, called MIZAR, have been in use for a decade for discrete mathematics instruction. We are concerned here with the features of the MIZAR language that that are used to diminish the gap between formal natural deduction and mathematical vernacular. The inference checking component of the validator can be easily changed. We demonstrate the influence on the way the expressive power of the language can be exploited by contrasting, for a fixed proposition, two proofs embodying the same idea but for which different checking modules have been used. The more powerful inference checker that we discuss incorporates the formalization of obviousness given by M. Davis.

UR - http://www.scopus.com/inward/record.url?scp=0343646385&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0343646385&partnerID=8YFLogxK

U2 - 10.1007/3-540-15648-8_30

DO - 10.1007/3-540-15648-8_30

M3 - Conference contribution

AN - SCOPUS:0343646385

SN - 9783540156482

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 406

EP - 412

BT - Logics of Programs , Proceedings

A2 - Parikh, Rohit

PB - Springer Verlag

T2 - Conference on Logic of Programs, 1985

Y2 - 17 June 1985 through 19 June 1985

ER -