Back to Search
Start Over
Conference paper
- Source :
- LICS
- Publication Year :
- 2019
- Publisher :
- arXiv, 2019.
-
Abstract
- 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. both standard and Henkin 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 both 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-Schonflukel-Ramsey fragment of HoCHC modulo a restricted form of Linear Integer Arithmetic.
- Subjects :
- Soundness
Discrete mathematics
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Horn clause
Modulo
0102 computer and information sciences
02 engineering and technology
Resolution (logic)
01 natural sciences
Higher-order logic
Decidability
Logic in Computer Science (cs.LO)
Fragment (logic)
010201 computation theory & mathematics
Completeness (logic)
Computer Science::Logic in Computer Science
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Mathematics
Subjects
Details
- Database :
- OpenAIRE
- Journal :
- LICS
- Accession number :
- edsair.doi.dedup.....eb7908e4c6bfb1b60c16b35a6bccc3a7
- Full Text :
- https://doi.org/10.48550/arxiv.1902.10396