Finding Finite Herbrand Models

Description

We show that finding finite Herbrand models for a restricted class of first-order clauses is ExpTime-complete. A Herbrand model is called finite if it interprets all predicates by finite subsets of the Herbrand universe. The restricted class of clauses consists of anti-Horn clauses with monadic predicates and terms constructed over unary function symbols and constants. The decision procedure can be used as a new goal-oriented algorithm to solve linear language equations and unification problems in the description logic FL₀. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.

Links & Downloads

1. urn:nbn:de:bsz:14-qucosa2-795243
2. 180937913X
3. https://tud.qucosa.de/id/qucosa%3A79524
4. https://tud.qucosa.de/api/qucosa%3A79524/attachment/ATT-0/

Tags

info:eu-repo/classification/ddc/004

ddc:004

Additional Fields

Identifer	oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:79524
Date	16 June 2022
Creators	Borgwardt, Stefan, Morawska, Barbara
Publisher	Technische Universität Dresden
Source Sets	Hochschulschriftenserver (HSSS) der SLUB Dresden
Language	English
Detected Language	English
Type	info:eu-repo/semantics/acceptedVersion, doc-type:report, info:eu-repo/semantics/report, doc-type:Text
Rights	info:eu-repo/semantics/openAccess
Relation	urn:nbn:de:bsz:14-qucosa2-785040, qucosa:78504