Sciweavers

TABLEAUX
2000
Springer
13 years 9 months ago
Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison
The aim of the TABLEAUX-2000 Non-Classical (Modal) System Comparisons (TANCS-2000) is to provide a set of benchmarks and a standardized methodology for the assessment and compariso...
Fabio Massacci, Francesco M. Donini
TABLEAUX
2000
Springer
13 years 9 months ago
Matrix-Based Inductive Theorem Proving
We present an approach to inductive theorem proving that integrates rippling-based rewriting into matrix-based logical proof search. The selection of appropriate connections in a m...
Christoph Kreitz, Brigitte Pientka
TABLEAUX
2000
Springer
13 years 9 months ago
Consistency Testing: The RACE Experience
Abstract. This paper presents the results of applying RACE, a description logic system for ALCNHR+ , to modal logic SAT problems. Some aspects of the RACE architecture are discusse...
Volker Haarslev, Ralf Möller
TABLEAUX
2000
Springer
13 years 9 months ago
Modality and Databases
Two things are done in this paper. First, a modal logic in which one can quantify over both objects and concepts is presented; a semantics and a tableau system are given. It is a n...
Melvin Fitting
TABLEAUX
2000
Springer
13 years 9 months ago
A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations
Abstract. In this paper we present a labelled proof method for computing nonmonotonic consequence relations in a conditional logic setting. The method is based on the usual possibl...
Alberto Artosi, Guido Governatori, Antonino Rotolo
18
Voted
TABLEAUX
2000
Springer
13 years 9 months ago
MSPASS: Modal Reasoning by Translation and First-Order Resolution
mspass is an extension of the first-order theorem prover spass, which can be used as a modal logic theorem prover, a theorem prover for description logics and a theorem prover for ...
Ullrich Hustadt, Renate A. Schmidt
TABLEAUX
2000
Springer
13 years 9 months ago
Benchmark Analysis with FaCT
FaCT (Fast Classification of Terminologies) is a Description Logic (DL) classifier that can also be used for modal logic satisfiability testing. The FaCT system includes two reason...
Ian Horrocks