Inhaltszusammenfassung

We present a synthesis of our previous work on symbol elimination in extensions of a theory T0 with additional function symbols whose properties are axiomatised using a set of clauses: We analyze situations in which we can perform such tasks in a hierarchical way, relying on existing mechanisms for symbol elimination in T0. This is for instance possible if the base theory allows quantifier elimination. We analyze possibilities of extending such methods to situations in which...We present a synthesis of our previous work on symbol elimination in extensions of a theory T0 with additional function symbols whose properties are axiomatised using a set of clauses: We analyze situations in which we can perform such tasks in a hierarchical way, relying on existing mechanisms for symbol elimination in T0. This is for instance possible if the base theory allows quantifier elimination. We analyze possibilities of extending such methods to situations in which the base theory does not allow quantifier elimination but has a model completion which does. We then briefly discuss the way the method can be used in the analysis of parametric systems (for synthesizing constraints on parameters and also for invariant synthesis) (Invited talk at FROM 2018)» weiterlesen» einklappen

Autoren

Klassifikation

DFG Fachgebiet:
Informatik

DDC Sachgruppe:
Informatik