Skip to main navigation Skip to search Skip to main content

Automating algebraic proofs in algebraic logic

  • National Taiwan University

Research output: Contribution to journalArticlepeer-review

Abstract

We present here an effective proof theory that allows one to reason within algebras of algebraic logic in a purely syntactic, algebraic fashion. We demonstrate the effectiveness of the method by discussing our automated proofs of problems and theorems taken from Professor Helena Rasiowa's book An Algebraic Approach to Non-Classical Logics, Studies in Logic and Fundation of Mathematics, Volume 78, North Holland Publishing Company, Amsterdam, London - PWN, Warsaw (1974). We include a detailed proof of a problem presented to us by Professor Helena Rasiowa in June 1993. Most of these proofs are the first direct proofs ever discovered, and they are produced by the computer without human assistance.

Original languageEnglish
Pages (from-to)129-140
Number of pages12
JournalFundamenta Informaticae
Volume28
Issue number1-2
DOIs
StatePublished - Nov 1996

Fingerprint

Dive into the research topics of 'Automating algebraic proofs in algebraic logic'. Together they form a unique fingerprint.

Cite this