A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains

L. Wos*, S. Winker, B. Smith, R. Veroff, L. Henschen

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

22 Scopus citations

Abstract

The field of automated reasoning is an outgrowth of the field of automated theorem proving. The difference in the two fields is not so much in the procedures on which they rest, but rather in the way the corresponding programs are used. Here we present a comprehensive treatment of the use of an automated reasoning program to answer certain previously open questions from equivalential calculus. The questions are answered with a uniform method that employs schemata to study the infinite domain of theorems deducible from certain formulas. We include sufficient detail both to permit the work to be duplicated and to enable one to consider other applications of the techniques. Perhaps more important than either the results or the methodology is the demonstration of how an automated reasoning program can be used as an assistant and a colleague. Precise evidence is given of the nature of this assistance.

Original languageEnglish (US)
Pages (from-to)303-356
Number of pages54
JournalArtificial Intelligence
Volume22
Issue number3
DOIs
StatePublished - Apr 1984

ASJC Scopus subject areas

  • Language and Linguistics
  • Linguistics and Language
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains'. Together they form a unique fingerprint.

Cite this