Semantisches Browsen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
LATPub491
Abstract We show that finding finite Herbrand model
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 FL0. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.
one which was even best-case exponential.  +
Author Stefan Borgwardt + , Barbara Morawska +
BibTex
@inproceedings{ BoMo-LPAR-12,
  address = {M{\'e}rida, Venezuela},
  author = {Stefan {Borgwardt} and Barbara {Morawska}},
  booktitle = {Proceedings of the 18th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR'12)},
  editor = {Nikolaj {Bj{\o}rner} and Andrei {Voronkov}},
  pages = {138--152},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Finding Finite {H}erbrand Models},
  volume = {7180},
  year = {2012},
}
Bibtype Inproceedings  +
Booktitle Proceedings of the 18th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR'12)  +
Download BoMo-LPAR-12.pdf  +
Editor Nikolaj Bjørner and Andrei Voronkov  +
ErsterAutorNachname Borgwardt  +
ErsterAutorVorname Stefan  +
Forschungsgruppe Automatentheorie +
Pages 138-152  +
Publication text Stefan Borgwardt, Barbara Morawska<br/&
Stefan Borgwardt, Barbara Morawska<br/> '''[[LATPub491|<b>Finding Finite Herbrand Models</b>]]''' <br/>__NOTOC__In Nikolaj Bjørner and Andrei Voronkov, eds., <i>Proceedings of the 18th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR'12)</i>, volume 7180 of Lecture Notes in Computer Science, 138-152, 2012. Springer<br/><span class="glyphicon glyphicon-chevron-right" style="font-size: 85%;" ></span> [[LATPub491|Details]] <span class="glyphicon glyphicon-chevron-right" style="font-size: 85%; margin-left: 2ex; "></span> [[Media:BoMo-LPAR-12.pdf|Download]]
an> [[Media:BoMo-LPAR-12.pdf|Download]]  +
Publication text en Stefan Borgwardt, Barbara Morawska<br/&
Stefan Borgwardt, Barbara Morawska<br/> '''[[LATPub491/en|<b>Finding Finite Herbrand Models</b>]]''' <br/>__NOTOC__In Nikolaj Bjørner and Andrei Voronkov, eds., <i>Proceedings of the 18th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR'12)</i>, volume 7180 of Lecture Notes in Computer Science, 138-152, 2012. Springer<br/><span class="glyphicon glyphicon-chevron-right" style="font-size: 85%;" ></span> [[LATPub491|Details]] <span class="glyphicon glyphicon-chevron-right" style="font-size: 85%; margin-left: 2ex;" ></span> [[Media:BoMo-LPAR-12.pdf|Download]]
an> [[Media:BoMo-LPAR-12.pdf|Download]]  +
Publisher Springer  +
Referiert 1  +
Series Lecture Notes in Computer Science  +
Title Finding Finite Herbrand Models  +
To appear 0  +
Type inproceedings  +
Volume 7180  +
Year 2012  +
Hat Abfrage
Dieses Attribut ist ein Spezialattribut in diesem Wiki.
LATPub491 + , LATPub491 + , LATPub491 + , LATPub491 + , LATPub491 + , LATPub491 +
Kategorien Inproceedings , Publikation
Zuletzt geändert
Dieses Attribut ist ein Spezialattribut in diesem Wiki.
25 März 2015 14:34:07  +
verstecke Attribute die hierhin verlinken 
LATPub491/en + Weiterleitungsseite
 

 

Bitte den Namen einer Seite angeben, um mit dem Browsen zu beginnen.