Differences

This shows you the differences between two versions of the page.

--- sav07_lecture_19 [2007/05/22 14:36]
vkuncak
+++ sav07_lecture_19 [2007/05/31 12:14]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Lecture 19 ======
+(Presented by Ruzica Piskac.)
 === Push-down automata ===
-=== First-order theorem provers: completeness of resolution ===
+Equivalence of push-down automata and context-free grammars.
+Intersection of a regular and context-free language.
+=== First-order theorem provers ===
+Completeness of propositional resolution.
+Undecidability of first-order logic.
+Completeness of first-order resolution.
+Slides:
+  * {{ganzingerbachmairconstructionslides.pdf|Ganzinger-Bachmair Model Construction}}
+  * {{priorityqueuesslides.pdf|Verifying a checker for priority queues}}