Grant: Discovery Grants Program - Individual

Predicate logic is used widely in Computer Science to formalise and prove properties of programs, specify the contents of a database, or represent a body of knowledge. A particular ""implementation"" of predicate logic-calculational logic-relies on Leibniz's principle of ""replacing equals by equals"" that allows the user to prove assertions in the same way that one verifies the equality of two expressions in high school algebra or trigonometry, namely, by calculating a chain of equalities. However, when we reason formally within calculational logic we often need to break our chain of equalities and invoke a rule that will spawn a new chain of equalities, disjoint from the original. This happens, for example, when one chain ends with an assertion A, and the new chain starts with the generalisation of said assertion, i.e., ""for all x, A"". While the verification of an assertion is equivalent to that of its generalisation, there is no formal way to write this down as an equality in classical logical calculus. On the other hand, the similarly sounding equality ""A = for all x, A"", that we can state within calculational logic, is invalid! Users of logic often stumble on this and related ""disconnecting"" steps in reasoning. Thus, one motivation for our research is methodological, to provide a more reliable framework for proving theorems-a kind of good engineering practise in logic. Another motivation relates to our choice of specific methodology (modal predicate logic), and is to contribute to the understanding and development of this fairly new area in logic, which unlike its well studied propositional counterpart is still under construction. The fundamental approach in our research has been to augment the expressive power of classical logic by adding the modal operator, so that we can now write a formal equality that says ""the verification of an assertion is equivalent to that of its generalisation"". Our research is also concerned with practical issues: We are carefully designing a ""practical"" calculational logic that will allow its end-user such as a student of computer science to reliably write correct, well annotated calculational proofs. This methodology may also find application in the areas of program verification and automated reasoning.