Recent PhD Theses - 2

Author	Suman Roy
Title	Soundness and Completeness Results in Partially-interpreted Logics
Thesis Supervisor	Vijaya Chandru
Date of Defence	6 November, 1998
Institute granting Degree	Indian Institute of Science, Bangalore
Current Address	Email: `suman@imsc.ernet.in`
	The Institute of Mathematical Sciences, Chennai 600 113

Abstract

Formulas in mathematical logic are syntactic expressions of uninterpreted symbols. The classical computational techniques of logic are oriented to 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 inference system in the language.

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, on Horn clauses, in a natural way. Using functions and certain predicates (called constraints) interpreted in a pre-defined computational domains (e.g., reals, booleans, finite and infinite trees), CLP has been able to successfully model 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 formal verification of physical systems. An important aspect of these logics is their ability to model the temporal behaviour 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.

Previous Thesis
Next Thesis