Kipler is an object-oriented tableau framework for rapid development of (modalized) description logic reasoners.It also comes with readily implemented decision procedures for some of these logics.
A decision procedure for such a logic can be implemented by (programmatically) extending the classes
... [More] provided by Kipler and thus making use of object-oriented programming techniques. It is not our aim to develop a general tableau definition language for these logics.
Kipler is under heavy development. Currently it supports SHIQ ABox reasoning and experimental SHOIQ reasoning. These logics are the underlying formalism of Web Ontology Language: OWL and thus are included in Kipler's profile to demonstrate its capabilities. These implementations also employ some optimization techniques, e.g., semantic branching and backjumping, to make them "practical". The facilities provided by Kipler for optimizations can be extended to modal description logics as well.
The first alpha version is planned to be released when integration with an OWL parsing API is completed and more tests are done.
The name Kipler means "modalities" in Turkish. [Less]
This is a project with the primary purpose to provide source code for Tableau [white|black|green]Board Processing.
The first algorithm developted is described on paper published on CBDAR 2007 in Curitiba, Brazil.
"Processing Teaching-Board Images Acquired with Portable Digital Cameras", Daniel
... [More] Oliveira, and Rafael Lins
You can download the PDF from this link http://www.m.cs.osakafu-u.ac.jp/cbdar2007/program.shtml#proc
Right now we are organizing the source code to add in the repository, if the you need it you can e-mail to danielmarquesoliveira at gmail dot com [Less]
This suite of tools consists of:
hylores : a resolution-based theorem prover for the hybrid logic H(@,A,D,◇¯,↓) htab : a tableaux-based theorem prover for the hybrid logic H(@,A,D,◇¯,↓) with role inclusion hylolib : the common library used by the other provers gridtest : a framework to test and
... [More] compare provers on a single machine or a grid These tools can be obtained from the Home page of the project. [Less]
tableau-parm is an small command line utility designed to interact with Tableau forensic write blockers. It performs functions similar to the Tableau Disk Monitor, except that it operates under select UNIX platforms.