Symbol Elimination and Applications to Parametric Entailment Problems
Konev, Boris ; Reger, Giles (Hrsg). Frontiers of Combining Systems : 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8–10, 2021, Proceedings. Cham: Springer International Publishing AG 2021 S. 43 - 62 (Lecture Notes in Artificial Intelligence ; 12941)
Erscheinungsjahr: 2021
ISBN/ISSN: 978-3-030-86204-6
Publikationstyp: Buchbeitrag (Konferenzbeitrag)
Sprache: Englisch
| Geprüft | Bibliothek |
Inhaltszusammenfassung
We analyze possibilities of second-order quantifier elimination for formulae containing parameters – constants or functions. For this, we use a constraint resolution calculus obtained from specializing the hierarchical superposition calculus. If saturation terminates, we analyze possibilities of obtaining weakest constraints on parameters which guarantee satisfiability. If the saturation does not terminate, we identify situations in which finite representations of infinite saturated sets exis...We analyze possibilities of second-order quantifier elimination for formulae containing parameters – constants or functions. For this, we use a constraint resolution calculus obtained from specializing the hierarchical superposition calculus. If saturation terminates, we analyze possibilities of obtaining weakest constraints on parameters which guarantee satisfiability. If the saturation does not terminate, we identify situations in which finite representations of infinite saturated sets exist. We identify situations in which entailment between formulae expressed using second-order quantification can be effectively checked. We illustrate the ideas on a series of examples from wireless network research.» weiterlesen» einklappen
Klassifikation
DFG Fachgebiet:
Informatik
DDC Sachgruppe:
Informatik
