Name
Abstract | ||
|---|---|---|
Some problems posed years ago remain challenging today. In particular, the Robbins problem, which is still open and which is the focus of attention in this paper, offers interesting challenges for attack with the assistance of an automated reasoning program; for the study presented here, we used the program OTTER. For example, when one submits this problem, which asks for a proof that every Robbins algebra is a Boolean algebra, a large number of deduced clauses results. One must, therefore, consider the possibility that there exists a Robbins algebra that is not Boolean; such an algebra would have to be infinite. One can instead search for properties that, if adjoined to those of a Robbins algebra, guarantee that the algebra is Boolean. Here we present a number of such properties, and we show how an automated reasoning program was used to obtain the corresponding proofs. Additional properties have been identified, and we include here examples of using such a program to check that the corresponding hand-proofs are correct. We present the appropriate input for many of the examples and also include the resulting proofs in clause notation. |
Year | DOI | Venue |
|---|---|---|
1990 | 10.1007/BF00244359 | J. Autom. Reasoning |
Keywords | Field | DocType |
universal algebra,automated theorem proving,automated reasoning,boolean algebra | Discrete mathematics,Stone's representation theorem for Boolean algebras,Allen's interval algebra,Algebra,Computer science,Robbins algebra,Algorithm,Boolean algebra,Boolean algebra (structure),Two-element Boolean algebra,Complete Boolean algebra,Free Boolean algebra | Journal |
Volume | Issue | ISSN |
6 | 4 | 0168-7433 |
Citations | PageRank | References |
17 | 3.25 | 7 |
Authors | ||
1 | ||