Computational Logic 320441 CompLog Lecture Notes - kwarc.info

Nov 18, 2015 - if there are problems send e-mail to me. ©:Michael ...... Links: href, src, ...limited, non- descriptive ...... ?person foaf:mbox ?email. } ©:Michael ...
2MB Sizes 1 Downloads 264 Views
Computational Logic 320441 CompLog Lecture Notes Michael Kohlhase School of Engineering & Science Jacobs University, Bremen Germany [email protected] office: Room [email protected] 1, phone: x3140 November 18, 2015

i

Preface Introduction The ability to represent knowledge about the world and to draw logical inferences is one of the central components of intelligent behavior. As a consequence, reasoning components of some form are at the heart of many artificial intelligence systems. Logic: The field of logic studies representation and inference systems. It dates back and has its roots in Greek philosophy as presented in the works of Aristotle and others. Since then logic has grown in richness and diversity over the centuries to finally reach the modern methodological approach first expressed in the work of Frege. Logical calculi, which capture an important aspect of human thought, were now amenable to investigation with mathematical rigour and the beginning of this century saw the influence of these developments in the foundations of mathematics, in the work of Hilbert, Russell and Whitehead, in the foundations of syntax and semantics of language, and in philosophical foundations expressed most vividly by the logicians in the Vienna Circle. Computational Logic: The field of Computational Logic looks at computational aspects of logic. It is essentially the computer-science perspective of logic. The idea is that logical statements can be executed on a machine. This has far-reaching consequences that ultimately lead to logic programming, deduction systems for mathematics and engineering, logical design and verification of computer software and hardware, deductive databases and software synthesis as well as logical techniques for analysis in the field of mechanical engineering. Logic Engineering: As all of these applications require efficient implementations of the underlying inference systems, computational logic focuses on proof theory much more than on model theory (which is the focus of mathematical logic, a neighboring field). As the respective applications have different requirements on the expressivity and structure of the representation language and on the statements derived or the terms simplified, computational logic focuses on “logic engineering”, i.e. the development of representation languages, inference systems, and module systems with specific properties.

Course Concept Aims: The course 320441 “Computational Logic” (CompLog) is a specialization course offered to third-year undergraduate students and to first-year graduate students at Jacobs University Bremen. The course aims to give these students a solid (and somewhat theoretically oriented) foundation of computational logic and logic engineering techniques. Prerequisites: The course makes very little assumptions about prior knowledge, but the learning curve is very steep for students who have no prior exposure to logic. As a consequence, the course has a prerequisite to the course 320211 Formal Languages and Logic which is a mandatory course in the Computer Science program at Jacobs University. This prerequisite can be waived by the instructor for other students. Course Contents: We carefully recap the foundations of first-order logic and present the tableau calculus as a computationally inspired inference procedure. Free variable tableaux also introduce unification, and important computational tool in logics. Finally, we introduce the model existence method for proving completeness of calculi. The next part of the course is about enhancing the expressivity of first-order logic to include functions, predicates, and sets. The intended application is a more adequate representation of mathematical concepts, where these objects are common. Here we introduce the simply typed λ calculus as the main representational vehicle, since it casts function comprehension into an equational theory which we show to be terminating, confluent, and complete. Thus we can build higher-order inference by extending unification and tabl