Independent axiom systems for nearlattices. (English) Zbl 1249.06003

There exist several axiom systems for nearlattices. The authors checked two of them, namely the axiom system by R. Hickman [Commun. Algebra 8, 1653–1685 (1980; Zbl 0436.06003)] and the other by Chajda et al. (see, e.g., [I. Chajda, R. Halaš and J. Kühr, Semilattice structures. Lemgo: Heldermann Verlag (2007; Zbl 1117.06001)]). They show that both systems are redundant and, using of the automated deduction tool Prover9, they found which of the axioms can be omitted. Moreover, they set up a new axiom system for nearlattices consisting of two axioms in five variables.


06A12 Semilattices
06B75 Generalizations of lattices
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)


Prover9; Mace4
Full Text: DOI arXiv EuDML Link


[1] I. Chajda, R. Halaš: An example of a congruence distributive variety having no near-unanimity term. Acta Univ. M. Belii Ser. Math. 13 (2006), 29–31. · Zbl 1132.08002
[2] I. Chajda, R. Halaš, J. Kühr: Semilattice structures. Research and Exposition in Mathematics 30, Heldermann Verlag, Lemgo, 2007.
[3] I. Chajda, M. Kolařík: Nearlattices. Discrete Math. 308 (2008), 4906–4913. · Zbl 1151.06004
[4] R. Hickman: Join algebras. Commun. Algebra 8 (1980), 1653–1685. · Zbl 0436.06003
[5] W. McCune: Prover9 and Mace4, version 2009-11A. ( http://www.cs.unm.edu/mccune/prover9/ ).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.