You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Automating Algebraic Proofs in Algebraic Logic

Article type: Research Article

Authors: Hsiang, Jieh | Wasilewska, Anita

Affiliations: Department of Computer Science, National Taiwan University, Taipei, Taiwan. hsiang@csie.ntu.edu.tw | Department of Computer Science, State University of New York at Stony Brook, Stony Brook, NY, USA. anita@sbcs.sunysb.edu

Note: [] Supported in part by grant NSC 95-2221-E-002-009 of the National Science Council of the Republic of China.

Note: [] Supported by Fulbright grant USIA 93-68818 (1993-1994).

DOI: 10.3233/FI-1996-281208

Journal: Fundamenta Informaticae, vol. 28, no. 1-2, pp. 129-140, 1996

Published: 1996
Get PDF

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.

Show more