•  1140
    In the domain of ontology design as well as in Knowledge Representation, modeling universals is a challenging problem.Most approaches that have addressed this problem rely on Description Logics (DLs) but many difficulties remain, due to under-constrained representation which reduces the inferences that can be drawn and further causes problems in expressiveness. In mathematical logic and program checking, type theories have proved to be appealing but, so far they have not been applied in the form…Read more
  •  5
    A Monadic Second-Order Version of Tarski’s Geometry of Solids
    Logic and Logical Philosophy 1-45. forthcoming.
    In this paper, we are concerned with the development of a general set theory using the single axiom version of Leśniewski’s mereology. The specification of mereology, and further of Tarski’s geometry of solids will rely on the Calculus of Inductive Constructions (CIC). In the first part, we provide a specification of Leśniewski’s mereology as a model for an atomless Boolean algebra using Clay’s ideas. In the second part, we interpret Leśniewski’s mereology in monadic second-order logic using nam…Read more
  •  4
    Goal reasoning with context record types
    with Patrick Barlatier
    In T. R. Roth-Berghofer D. C. Richardson B. Kokinov (ed.), Modeling and Using Context, Springer. pp. 164--177. 2007.