View/Download
Even though the main emphasis of the book is on the design of procedures for constructing formal proofs, the treatment of the semantics is perfectly rigorous. The following paradigm has been followed: Having defined the syntax of the language, it is shown that the set of well-formed formulae is a freely generated inductive set. This is an important point, which is often glossed over. Then, the concepts of satisfaction and validity are defined by recursion over the freely generated inductive set (using the 'unique homomorphic extension theorem', which can be rigorously justified). Finally, the proof theory is developped, and procedures for constructing proofs are given. Particular attention is given to the complexity of such procedures.Added by clownfish on 2007-01-05 06:15:14
View/Download