On the Logical Content of Logic Programs
This work provides new insights into the logical foundations of logic programming, with potential applications in knowledge representation, automated reasoning, and formal verification, but it is incremental as it builds on existing proof-theoretic semantics.
The paper tackles the problem of interpreting the logical content of logic programs by introducing a novel 'support' relation that explicates what a program 'knows', showing it can express classical, intuitionistic, and intermediate logics depending on choices in logic programming semantics.
Logic programming (LP) is typically understood through operational semantics (e.g., SLD-resolution) or model-theoretic interpretations (e.g., the least Herbrand model). This paper introduces a novel perspective on LP by defining a ``support'' relation that explicates what a program ``knows''. This interpretation is shown to express classical and intuitionistic logic, as well as an intermediate logic, depending on certain choices regarding LP and the meanings of disjunction and negation. These results are formalized using the idea of base-extension semantics within proof-theoretic semantics. Our approach offers new insights into the logical foundations of LP and has potential applications in knowledge representation, automated reasoning, and formal verification.