LETHE: A Saturation-Based Tool for Non-Classical Reasoning

P Koopmann; R A Schmidt; M Dumontier; B Glimm; R Goncalves; M Horridge; E Jiménez-Ruiz; N Matentzoglu; B Parsia; G Stamou; G Stoilos

LETHE: A Saturation-Based Tool for Non-Classical Reasoning

P Koopmann, R A Schmidt, M Dumontier (Editor), B Glimm (Editor), R Goncalves (Editor), M Horridge (Editor), E Jiménez-Ruiz (Editor), N Matentzoglu (Editor), B Parsia (Editor), G Stamou (Editor), G Stoilos (Editor)

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

82 Downloads (Pure)

Abstract

We present the saturation-based reasoning system LETHE.LETHE is a tool that can be used for uniform interpolation, forgetting,TBox abduction and logical difference. To solve these problems, LETHEuses saturation-based reasoning to eliminate certain symbols from an ontology,such that entailments in the remaining vocabulary are preserved.This is known as forgetting or uniform interpolation. LETHE is an implementationof our forgetting methods for various expressive descriptionlogics, and can be used as a Java library and as a standalone tool forthe mentioned reasoning tasks. We give a high level description of thecalculi used by LETHE, describe the reasoning algorithm implemented inLETHE, and give an evaluation of the system on realistic ontologies.

Original language	English
Title of host publication	Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015)
Editors	M Dumontier, B Glimm, R Goncalves, M Horridge, E Jiménez-Ruiz, N Matentzoglu, B Parsia, G Stamou, G Stoilos
Publisher	RWTH Aachen University
Volume	1387
Publication status	Published - 2015

Publication series

Name	CEUR Workshop Proceedings

Access to Document

FULL-TEXT

Cite this

Koopmann, P., Schmidt, R. A., Dumontier, M. (Ed.), Glimm, B. (Ed.), Goncalves, R. (Ed.), Horridge, M. (Ed.), Jiménez-Ruiz, E. (Ed.), Matentzoglu, N. (Ed.), Parsia, B. (Ed.), Stamou, G. (Ed.), & Stoilos, G. (Ed.) (2015). LETHE: A Saturation-Based Tool for Non-Classical Reasoning. In M. Dumontier, B. Glimm, R. Goncalves, M. Horridge, E. Jiménez-Ruiz, N. Matentzoglu, B. Parsia, G. Stamou, & G. Stoilos (Eds.), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015) (Vol. 1387). (CEUR Workshop Proceedings). RWTH Aachen University. http://ceur-ws.org/Vol-1387/paper_9.pdf

Koopmann, P ; Schmidt, R A ; Dumontier, M (Editor) et al. / LETHE: A Saturation-Based Tool for Non-Classical Reasoning. Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). editor / M Dumontier ; B Glimm ; R Goncalves ; M Horridge ; E Jiménez-Ruiz ; N Matentzoglu ; B Parsia ; G Stamou ; G Stoilos. Vol. 1387 RWTH Aachen University, 2015. (CEUR Workshop Proceedings).

@inproceedings{50b66532e7c04dd89f78b4da5572fbb3,

title = "LETHE: A Saturation-Based Tool for Non-Classical Reasoning",

abstract = "We present the saturation-based reasoning system LETHE.LETHE is a tool that can be used for uniform interpolation, forgetting,TBox abduction and logical difference. To solve these problems, LETHEuses saturation-based reasoning to eliminate certain symbols from an ontology,such that entailments in the remaining vocabulary are preserved.This is known as forgetting or uniform interpolation. LETHE is an implementationof our forgetting methods for various expressive descriptionlogics, and can be used as a Java library and as a standalone tool forthe mentioned reasoning tasks. We give a high level description of thecalculi used by LETHE, describe the reasoning algorithm implemented inLETHE, and give an evaluation of the system on realistic ontologies.",

author = "P Koopmann and Schmidt, {R A} and M Dumontier and B Glimm and R Goncalves and M Horridge and E Jim{\'e}nez-Ruiz and N Matentzoglu and B Parsia and G Stamou and G Stoilos",

year = "2015",

language = "English",

volume = "1387",

series = "CEUR Workshop Proceedings",

publisher = "RWTH Aachen University",

editor = "M Dumontier and B Glimm and R Goncalves and M Horridge and E Jim{\'e}nez-Ruiz and N Matentzoglu and B Parsia and G Stamou and G Stoilos",

booktitle = "Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015)",

address = "Germany",

}

Koopmann, P, Schmidt, RA, Dumontier, M (ed.), Glimm, B (ed.), Goncalves, R (ed.), Horridge, M (ed.), Jiménez-Ruiz, E (ed.), Matentzoglu, N (ed.), Parsia, B (ed.), Stamou, G (ed.) & Stoilos, G (ed.) 2015, LETHE: A Saturation-Based Tool for Non-Classical Reasoning. in M Dumontier, B Glimm, R Goncalves, M Horridge, E Jiménez-Ruiz, N Matentzoglu, B Parsia, G Stamou & G Stoilos (eds), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). vol. 1387, CEUR Workshop Proceedings, RWTH Aachen University. <http://ceur-ws.org/Vol-1387/paper_9.pdf>

LETHE: A Saturation-Based Tool for Non-Classical Reasoning. / Koopmann, P; Schmidt, R A; Dumontier, M (Editor) et al.
Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). ed. / M Dumontier; B Glimm; R Goncalves; M Horridge; E Jiménez-Ruiz; N Matentzoglu; B Parsia; G Stamou; G Stoilos. Vol. 1387 RWTH Aachen University, 2015. (CEUR Workshop Proceedings).

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - LETHE: A Saturation-Based Tool for Non-Classical Reasoning

AU - Koopmann, P

AU - Schmidt, R A

A2 - Dumontier, M

A2 - Glimm, B

A2 - Goncalves, R

A2 - Horridge, M

A2 - Jiménez-Ruiz, E

A2 - Matentzoglu, N

A2 - Parsia, B

A2 - Stamou, G

A2 - Stoilos, G

A2 - Dumontier, M

A2 - Glimm, B

A2 - Goncalves, R

A2 - Horridge, M

A2 - Jiménez-Ruiz, E

A2 - Matentzoglu, N

A2 - Parsia, B

A2 - Stamou, G

A2 - Stoilos, G

PY - 2015

Y1 - 2015

N2 - We present the saturation-based reasoning system LETHE.LETHE is a tool that can be used for uniform interpolation, forgetting,TBox abduction and logical difference. To solve these problems, LETHEuses saturation-based reasoning to eliminate certain symbols from an ontology,such that entailments in the remaining vocabulary are preserved.This is known as forgetting or uniform interpolation. LETHE is an implementationof our forgetting methods for various expressive descriptionlogics, and can be used as a Java library and as a standalone tool forthe mentioned reasoning tasks. We give a high level description of thecalculi used by LETHE, describe the reasoning algorithm implemented inLETHE, and give an evaluation of the system on realistic ontologies.

AB - We present the saturation-based reasoning system LETHE.LETHE is a tool that can be used for uniform interpolation, forgetting,TBox abduction and logical difference. To solve these problems, LETHEuses saturation-based reasoning to eliminate certain symbols from an ontology,such that entailments in the remaining vocabulary are preserved.This is known as forgetting or uniform interpolation. LETHE is an implementationof our forgetting methods for various expressive descriptionlogics, and can be used as a Java library and as a standalone tool forthe mentioned reasoning tasks. We give a high level description of thecalculi used by LETHE, describe the reasoning algorithm implemented inLETHE, and give an evaluation of the system on realistic ontologies.

M3 - Conference contribution

VL - 1387

T3 - CEUR Workshop Proceedings

BT - Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015)

PB - RWTH Aachen University

ER -

Koopmann P, Schmidt RA, Dumontier M, (ed.), Glimm B, (ed.), Goncalves R, (ed.), Horridge M, (ed.) et al. LETHE: A Saturation-Based Tool for Non-Classical Reasoning. In Dumontier M, Glimm B, Goncalves R, Horridge M, Jiménez-Ruiz E, Matentzoglu N, Parsia B, Stamou G, Stoilos G, editors, Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). Vol. 1387. RWTH Aachen University. 2015. (CEUR Workshop Proceedings).

LETHE: A Saturation-Based Tool for Non-Classical Reasoning

Abstract

Publication series

Access to Document

Fingerprint

Cite this