Automatikus tételbizonyítás
		Next

Automatikus tételbizonyítás

előadások

Várterész Magda

Kádek Tamás

Table of Contents

1. Előszó

2. Bevezetés

2.1. Az elsőrendű nyelv szintaxisa
2.2. Az elsőrendű nyelv klasszikus szemantikája
2.3. Logikai kalkulusok

3. Helyettesítések

3.1. Változók helyettesítése termekkel
3.2. Illesztő helyettesítés
3.3. Feladatok

4. Normálformák

4.1. Konjunktív és diszjunktív normálformák
4.2. Prenex alakú formulák
4.3. Skolem-normálforma
4.4. Elsőrendű klózok
4.5. Feladatok

5. Frege stílusú kalkulus

5.1. A predikátumkalkulus
5.2. Feladatok

6. Gentzen kalkulusai

6.1. A természetes levezetés
6.2. A szekventkalkulus
6.3. Feladatok

7. A rezolúciós kalkulus

7.1. A Herbrand-univerzum és az elsőrendű klózhalmazok

7.2. Az alaprezolúció

7.3. Az elsőrendű rezolúció

7.4. Rezolúciós levezetési stratégiák

7.4.1. 1. A teljes szintek módszere
7.4.2. 2. A törlési stratégia

7.5. Feladatok

Hivatkozások

List of Tables

3.1.
4.1. asszociativitás
4.2. kommutativitás
4.3. disztributivitás
4.4. idempotencia
4.5. elimináció (elnyelés)
4.6. De Morgan törvényei
4.7. kiszámítási törvények
4.8. logikai jelek közötti összefüggések
4.9. kétszeres tagadás
4.10. negáció az implikációban
4.11. kvantoros De Morgan-törvények
4.12. kvantorok egyoldali kiemelése,
4.13. kvantorok kétoldali kiemelése
4.14. kvantorhatáskör-átjelölés,
7.1.
7.2.
7.3.
7.4.
7.5.
7.6.
7.7.
7.8.
7.9.
7.10.
7.11.
7.12.
7.13.
7.14.

List of Equations

		Next
		Chapter 1. Előszó