Soundness and completeness results in partially-interpreted logics

Abstract

Formulas in mathematical logic are syntactic expressions of uninterpreted symbols. The classical computational techniques of logic are oriented toward establishing the truth or falsehood of logic formulas in their uninterpreted forms. To use logic as a language for modeling and analyzing real systems requires every aspect of the system to be abstracted from axiomatic principles. This makes pure or uninterpreted logic impractical for modern uses. The compromise that is often made is to admit partially interpreted functions and predicate symbols in the language to improve both expressiveness and efficiency of the inference system. Soundness and completeness show the equivalence of syntactic proof methods and the semantics of the logic, and are therefore fundamental properties that we expect of any logic applied to problems in computer science. The Constraint Logic Programming (CLP) scheme is a formal framework that extends traditional logic programming, based on Horn clauses, in a natural way. Using functions and certain predicates (called constraints) interpreted in predefined computational domains (e.g., reals, booleans, finite and infinite trees), CLP has successfully modeled many practical problems. More importantly, the scheme provides an orchestration of highly efficient solvers from these interpreted domains in carrying out inference tasks. Negation as (finite) failure is a fundamental technique for implementing default reasoning in the context of logic programming. In part one of the thesis, we give a resolution proof of the soundness and completeness of negation as failure in the framework of CLP. Real-time logics have been proposed in recent years to support the formal specification and verification of physical systems. An important aspect of these logics is their ability to model the temporal behavior of such systems. This is facilitated in real-time logics by assuming “time" to belong to the domain of natural or real numbers and by assuming interpretations of function and predicate symbols (as in arithmetic). In part two of the thesis, we investigate two real-time logics called Neighbourhood Logic (NL) and its extension Duration Calculus. We also propose a sound and relatively complete proof system for Duration Calculus.