de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Superposition for Fixed Domains

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44642

Horbach,  Matthias
Automation of Logic, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Horbach, M., & Weidenbach, C. (2010). Superposition for Fixed Domains. ACM Transactions on Computational Logic, 11(4): 27, pp. 27,1-27,35. doi:10.1145/1805950.1805957.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-14C3-6
Zusammenfassung
Disunification is an extension of unification to first-order formulae over syntactic equality atoms. Instead of considering only syntactic equality, I extend a disunification algorithm by Comon and Delor to ultimately periodic interpretations, i.e.~minimal many-sorted Herbrand models of predicative Horn clauses and, for some sorts, equations of the form $s^\upmb(x)\eq s^\upma(x)$. The extended algorithm is terminating and correct for ultimately periodic interpretations over a finite signature and gives rise to a decision procedure for the satisfiability of equational formulae in ultimately periodic interpretations. As an application, I show how to apply disunification to compute the completion of predicates with respect to an ultimately periodic interpretation. Such completions are a key ingredient to several inductionless induction methods.