We study general lattices with normal unary operators for which we prove relational representation and duality results. Similar results have appeared in print, using Urquhart’s lattice representation, by the second author with Vakarelov, Radzikowska and Rewitzky. We base our approach in this article on the Hartonas and Dunn lattice duality, proven by Gehrke and Harding to deliver a canonical lattice extension, and on recent results by the first author on the relational representation of normal lattice operators. We verify that the operators at the representation level (appropriately generated by relations) are the canonical extensions of the lattice operators, in Gehrke and Harding’s sense.

Dicomplemented lattices were introduced as an abstraction of Wille’s concept algebras which provided negations to a concept lattice. We prove a discrete representation theorem for the class of dicomplemented lattices. The theorem is based on a topology free version of Urquhart’s representation of g eneral lattices.

In previous work we have presented a class of algebras enhanced with two contact relations representing rough set style approximations of a spatial contact relation. In this paper, we develop a class of relational systems which is mutually interpretable with that class of algebras, and we consider a relational logic whose semantics is determined by those relational systems. For this relational logic we construct a proof system in the spirit of Rasiowa-Sikorski, and we outline the proofs of its soundness and completeness.

Rough relation algebras are a generalization of relation algebras such that the underlying lattice structure is a regular double Stone algebra. Standard models are algebras of rough relations. A discrete duality is a relationship between classes of algebras and classes of relational systems (frames). In this paper we prove a discrete duality for a class of rough relation algebras and a class of frames.

In this paper we show that the problem of discrete duality can be extended beyond the clasical setting of duality between a class of algebras and a class of relational structures. Namely, for some classes of algebras, the relevant dual structures are the structures with multirelations. Several applications of multirelations will be described.

We show that a logical formalism of binary relations can serve as a tool for specification and verification of a variety of tasks in the formal concept analysis.

A calculus of typed relations subsuming the classical relational database theory is presented. An associated sound and complete deduction mechanism is developed. The formulation is generalized to deal with nondeterministic databases and information relations in the rough set-style.

A semantics of identity inspired by rough set modeling of uncertainty is proposed and the underlying substitutivity principles are presented. A survey of some theories of identity is given, in particular, an interpretation of identity in E-unificatio

The purpose of this paper is to define and investigate document retrieval strategies based on rough sets. A subject classification index is modelled by means of a family of set-theoretic information systems. The family induces a power set hierarchy b

In order to provide a background for rough set modeling of uncertainty, two types of incompleteness of information are discussed. Representation of uncertain knowledge acquired from incomplete information is outlined within the framework of information logics. Relational proof theory for the information logics is presented. It is shown how these logics and their proof systems can be handled in the GLEFATINF (Graphical & Logical Editing Framework) system. This computer program is a key component of the inference laboratory Atelier d'Inféence (ATINF) developed at LIFIA‐IMAG, our lab. It provides a general framework, independent of logic and proof systems, for combining inference tools, editing, and checking proofs. The basic principles of its design and implementation are given and its capabilities are discussed. Its application to define the information logics and their proof systems and to present proofs in these proof systems is discussed and illustrated.

Abstract A method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.