Distinction-based and verification-assisted knowledge modeling

This position paper presents a lightweight approach for knowledge modeling centered around the notion of distinction. Concept models are represented using UML class diagrams. Distinctions between concepts are established by using attributes and stating properties of the attributes using the @L-is calculus on words. This calculus relies on simple laws to manipulate relationships between words. We show how to represent these concept models in ALLOY, a symbolic model checker for first-order logic, which allows one to verify the consistency and completeness of a concept model.