Introduction

For the course Multi-Agent Systems (2011-2012) we had to do a final project. As project subject, we've chosen to extend OOPS, an Object Oriented Prover for S5n, to support additional axiom systems. This website is a part of the project and contains all the information about our project.

OOPS ( Object Oriented Prover for S5n ) is made by Gert van Valkenhoef and Elske van der Vaart, they developed OOPS for their final project for the course Multi-agent Systems in 2007.
 OOPS is a Java-based implementation of semantic tableaux, which is an algorithm to automatically determine if a given logical formula is satifiable or not. OOPS implements this to determine formulas whether formulas are provable in S5n axiom system. The original version of OOPS was run from the command-line and would return true or false, meaning provable or not provable, in response to a given S5n formula.

The latest version of OOPS was made in 2009 and this version has a GUI (Graphical User Interface), and uses Lua scripts to handle the input of formulas. More information on the use of Lua and the notation of formulas can be found page Lua and formulas.

On this webpage, we present an extension of OOPS, where we implemented additional axiom systems and operators to further extend the capabilities of OOPS

The participants of this project are Lourens Elzinga and Rik Timmers.

 

The new version of OOPS can be downloaded here

The source code for the extended version of OOPS can be found here: https://github.com/woutgg/oops (See the commit log to find our changes)

The documentation and source code from OOPS made by Gert van Valkenhoef and Elske van der Vaart can be found here: https://github.com/gertvv/oops/wiki/Documentation

Copyright (c)2012 Extending OOPS to support additional axiom schemes
Powered by: Best Web Hosting and Affiliate Programs Directory. Created with Free Website Builder