CZ.1.07/2.2.00/28.0209 Elektronické opory a e-learning pro obory výpočtového a konstrukčního charakteru

- To pass, there are four preconditions

- 6 homeworks, open on Mondays. Two trials, the better is counted. Max. 4
p. per homework,

answer correct/incorrect/missing 1 unit /-0.5 unit /-0.25 unit, and

unit=4/NumberOfQuestions where NumberOfQuestions can vary (mostly between 10 and 20 per the homework)

- 1. introductory (in the 1st exercises, necessary to write, no points to
the evaluation);

2. supervised (at a lecture time)

3. final (in the last exercises, necessary to write, no points to the evaluation)

- 2 examples - a tableaux proof and maybe something else.

**Final exam** (40 p.)

- Anil Nerode, Richard A. Shore.

Shan-Hwei Nienhuys-Cheng, Ronald de Wolf.

Graham Priest.

Encyclopedia of database systems (Datalog, Executable knowledge).

- D. Gabbay, C. Hogger, J.A.Robinson.

Luc De Raedt.

Graham Priest.

Contents

- Introduction (pdf)
- Prerequisities. Resolution. Flavour of Prolog (1 lesson)
- Propositional and predicate logic (pdf)
- On satisfiability (ps)
(pdf)
(ps
4 pages).

Resolution in predicate logic (pdf) (animation) - SAT problem. Davis-Putnam Algorithm (pdf)
Animation

DPvis Visualizing Davis-Putnam Procedure - Logic programming and Prolog (ps) (pdf) (ps 4pages)

- Prolog and inference (1 lesson)
- Box model. Metainterpreters (ps)
(pdf)
(ps
4pages)

Backward chaining. Forward chaining (pl) - Knowledge-based systems (pdf)

Mycin

The Certainty-Factor Model

Certainty factor. How to

- Multi-agent systems
**Readings:**

Book on Decision procedures

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)*

- Box model. Metainterpreters (ps)
(pdf)
(ps
4pages)
- Deduction (1 lesson)
- Induction (3 lessons)
- Non-classical logic, knowledge representation and reasoning (2 lessons)
- 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)
- Present and future of computational logic (1 lesson)

Other links

- Is
there a Logic of Exploratory Data Analysis?

Committee on Logic Eduction of 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 Academia 2002

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