HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories
We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC) - a system of higher-order logic modulo theories - and prove its soundness and refutational completeness w.r.t. the standard semantics. As corollaries, we obtain the compactness theorem and semi-decidability of HoCHC for semi-decidable background theories, and we prove that HoCHC satisfies a canonical model property. Moreover a variant of the well-known translation from higher-order to 1st-order logic is shown to be sound and complete for HoCHC in standard semantics. We illustrate how to transfer decidability results for (fragments of) 1st-order logic modulo theories to our higher-order setting, using as example the Bernays-Schönfinkel-Ramsey fragment of HoCHC modulo a restricted form of Linear Integer Arithmetic.
Slides for "HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories" (HCVS19-HoCHC.pdf) | 608KiB |
Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:30 | |||
09:00 60m | Invited Talk: Concolic testing of higher-order functional languages HCVS Konstantinos (Kostis) Sagonas Uppsala University File Attached | ||
10:00 30mTalk | HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories HCVS Pre-print File Attached |