Computational Logic

Computational Logic

Evaluation

Questionnaire

Intrasemestral Exam

Test (contains also questions from the introductory Questionnaire) + Examples in April 12

Final exam

Thursday May 26 10-12 Monday June 6 10-12 Tuesday June 14 11-13 Monday June 27 10-12

F < 50, E < 60, D < 70, C < 80, B < 90, A >=90 Teaching material

Logic for Applications

Handbook of Logic in Artificial Intelligence and Logic Programming

Foundations of Inductive Logic Programming

An Introduction to Non-Classical Logic

Encyclopedia of database systems

Accesible form FI MU computer networks or via proxies. For more info see MU Libraries web page, Electronic Information Sources.

Additional readings

Logical And Relational Learning

Logic: A Very Short Introduction (Logika. Pruvodce pro każdého)

Exercises (here) (ilp)

Contents

Introduction (pdf)
Prerequisities (2 lessons)
- Propositional and predicate logic (ps) (pdf) (ps 4 pages)
- Resolution (ps) (pdf) (ps 4pages) (animation)
- Logic programming and Prolog (ps) (pdf) (ps 4pages)
Prolog. Inference I (1 lesson)
- Box model. Metainterpreters (ps) (pdf) (ps 4pages)
- Executable knowledge and Knowledge-based systems. Basic concepts (pdf)
  Backward chaining. Forward chaining (pl)
- Readings:
  Automated Reasoning: Sequent deduction. Natural deduction. In Stanford Encyclopedia of Philosophy
  Executable knowledge. In Encyclopedia of database systems
- And more (not for an exam): Overview of Automated Reasoning by Peter Baumgartner (at SSLI 2009)
Deduction (2 lessons)
On satisfiability (ps) (pdf) (ps 4 pages)
SAT problem. Davis-Putnam Algorithm (pdf) Animation
DPvis Visualizing Davis-Putnam Procedure
Tableau Proofs (ps) (pdf) (ps 4 pages) +PM
Animations for propositional and predicate logic.
LeanTAP, SWI Prolog implementation of a tableau prover
Deductive databases and Datalog (intro) (datalog)
Readings:
Automated Reasoning: Applications
Datalog. In Encyclopedia of Database Systems
Induction (3 lessons)
Inductive inference in propositional logic (ppt)
Classification (ppt)
Version spaces (Animation)
Decision tree learning (Animation I) (Animation II)
Inductive logic programming I (pdf) II (pdf)
Inverse resolution by Naren Ramakrishnan
Inductive synthesis of logic programs
Model Inference Problem (PM)
Model Inference System (Ehud Shapiro)
Assumption-based reasoning (ps) (pdf) and assumption-based learning (here)
Learning frequent patterns
Non-classical logic, knowledge representation and reasoning (2 lessons)
Modal logic and Tableau proofs (ps) (pdf) (ps 4 pages) (Animation)
Temporal logics (PM)
Non-classical logics at fiit stu (lecture 9 and 10)
Inference II. Reasoning with uncertainty
Logics for spatial and spatiotemporal data
Inductive inference in spatiotemporal logic (ps) (pdf)
Non-monotonic reasoning (pdf) by Jan Šefránek in Znalosti'05
Logic for natural language processing (1 lesson)
- Introduction to NLP
- Representing text in Prolog
- Definite Clause Grammars(dcg.pl)
- Transformation-based tagger
- Constraint grammars
- Multirelational learning of a part-of-speech tagger
Description logic and Semantic web (1 lesson)
Description Logic
Franz Baader. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, 2007. ISBN-13: 978-0521781763.
Enrico Franconi's course and other courses
Intro to Semantic Web
RDF, Fresnel (Display Vocabulary for RDF)
OWL, OIL, DAML+OIL

PM - will be available in Pavel Mareček's bookshop

Test (2005)

Other links

Committee on Logic Eduction

Association for Symbolic Logi

Logic Tutorials and Animations

Encyclopedia of Database Systems

summa logicae

Computational Logic Univ. of Madrid

V. Svejdar, Logika: neuplnost, slozitost a nutnost

Mathematical modal logic. A view of its evolution
Temporal Logic Stanford Encyclopedia fo Philosophy
Temporal Logic by Yde Venema
Notes on games in temporal logic by Ian Hodkinson
Linear-time Temporal Logic
Non-classical logics: theory and applications by Esko Turunen, Tampere University of Technology, Finland

Artificial Intelligence by Alison Cawsey at Heriot Watt
ACM Transactions on Computational Logic Scope of the Journal
Advanced Artificial Intelligence (uiowa)
Logic of learning by Peter Flach
Inductive inference and Kolmogorov complexity by Li and Vitanyi
John Lloyd
Knowledge Representation and Reasoning, Univ. of Leeds
Stanford Encyclopedia of Philosophy
Qualitative Spatial Reasoning in Univ. Leeds
J. Ullman's courses
Prover9 and Mace4 Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.
Foundational Ontology by Brandon Bennett
Macintosh Software for Logic and Branden Fitelsen's web site
John McCarthy
CL in Stanford A rigorous introduction to logic from a computational perspective. The course covers propositional logic and relational logic. Topics include syntax, semantics, models, logical entailment, proofs, soundness, completeness, and decidability. Reasoning methods include the truth table method, natural deduction, the Davis-Putnam procedure, resolution, model elimination, demodulation, and paramodulation.
Logics for knowledge representation and reasoning
SAT @ Delft This site contains various sorts of documented research, focused around the satisfiability area, which was carried out at Delft University

Czech version, old and incomplete