Computer aided reasoning

Andrzej Trybulec, Howard A. Blair

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationLogics of Programs , Proceedings
EditorsRohit Parikh
PublisherSpringer Verlag
Pages406-412
Number of pages7
ISBN (Print)9783540156482
DOIs
StatePublished - Jan 1 1985
EventConference on Logic of Programs, 1985 - Brooklyn, United States
Duration: Jun 17 1985Jun 19 1985

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume193 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherConference on Logic of Programs, 1985
CountryUnited States
CityBrooklyn
Period6/17/856/19/85

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Computer aided reasoning'. Together they form a unique fingerprint.

  • Cite this

    Trybulec, A., & Blair, H. A. (1985). Computer aided reasoning. In R. Parikh (Ed.), Logics of Programs , Proceedings (pp. 406-412). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 193 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-15648-8_30