Logikai kalkulusok egységes tárgyalása, és alkalmazása az oktatásban

Logikai kalkulusok egységes tárgyalása, és alkalmazása az oktatásban

Logikai kalkulusok egységes tárgyalása, és alkalmazása az oktatásban Kádek Tamás Témavezető: Dr. Várterész Magda

Kádek Tamás, Debreceni Egyetem, Informatikai Kar

2013.

1 / 18


Mérföldkövek • Matematikai logika példatár / Kádek Tamás, Robu Judit, Várterész Magda Cluj-Napoca : Presa Universitara Clujeana, 2010 • Gentzen-levezetések generálása oktatási célú számítógépes támogatással SzámOkt 2011 (20.) (2011) (Cluj-Napoca, Románia). - SzámOkt 2011: XX. Nemzetközi számítástechnika és oktatás konferencia. - p. 136-139. • Press-ready Deduction Trees in Classical Logic Using Point-Plus-Expressions Annales Universitatis Scientiarum Budapestinensis de Rolando Eötvös Nominatae. Section Computatorica. - 37 (2012), p. 229-238. Zbl 1249.03003


2013.

2 / 18


A GenTreeCad alkalmazás jellemzői • a formulák megadása a GenTreeCad alkalmazáson belül a LaTeX rendszerben megszokott képletek formájában történik, ennek előnye, hogy a kidolgozott LaTeX anyagokból egyszerűen átemelhető, • a formulát az alkalmazásban szerkezeti fájának segítségével tároljuk, mely további feldolgozásokat tesz lehetővé, • a formulák a kimeneten PDF formájában jelennek meg, így nincs szükség további grafikus utófeldolgozásra (ha szükséges a közbenső METAPOST és LaTeX források is elérhetők), • a bemenet (a formula) célszerűen szintén LaTeX képlet.


2013.

3 / 18


GenTreeCad alkalmazás Példa, az alkalmazás futtatásának eredménye:

X, Y → X

Y → Y, X

X→Y ⊃X

→ Y, Y ⊃ X

→ ¬X, Y ⊃ X

¬Y → Y ⊃ X

¬X ⊃ ¬Y → Y ⊃ X → (¬X ⊃ ¬Y ) ⊃ (Y ⊃ X)


2013.

4 / 18


Egységes tárgyalás – Pont-plusz-kifejezések ítéletlogikában Ha A egy formula, úgy • tA és • fA is címkézett formula. A pont-plusz-kifejezések P halmaza a legszűkebb olyan halmaz, mely tartalmazza a következőket: • címkézett formulák, • valamint, ha P1 P P, P2 P P, . . . , Pn P P (n ě 2), akkor – pP1 ˝ P2 ˝ ¨ ¨ ¨ ˝ Pn q és – pP1 ` P2 ` ¨ ¨ ¨ ` Pn q kifejezéseket.


2013.

5 / 18


Átírási algoritmus Legyen C ítéletlogikai formula. Definiáljuk a C formula pp-kifejezés alakját az alábbi szabályok használatával, a f C címkézett formulából. Addig alkalmazzuk a szabályokat, míg van olyan címkézett formula a pp-kifejezésben, melynek fő logikai összekötőjele ^ vagy _ vagy . (A és B formulákat jelöl). 1. f A ^ B ñ f A ` f B, 2. f A _ B ñ f A ˝ f B, 3. f A ñ tA. Tulajdonképpen az átírási algoritmus alkalmazásával csak helyettesítettük a konjunkciókat, diszjunkciókat és negációkat a `, a ˝, és a t szinbólummal. Megjegyzendő, hogy ha C konjunktív normál forma volt, akkor az algoritmus kimenete logikai összekötőjelek nélküli pp-kifejezés.


2013.

6 / 18


Pont-plusz rezolúció A pp-rezolúció axiómasémája: f X ` tX

és Γ ` f X ` tX

ahol Γ egy elemi plusz normál forma, és X egy propozícionális betű. A Pont-plus rezolúció kiterjesztési szabálya: ∆1 ` ∆2 ` ∆ ∆ 1 ` ∆2

és

Γ ` ∆1 ` ∆2 ` ∆ Γ ` ∆1 ` ∆2

ahol Γ egy elemi plusz normál forma. ∆1 és ∆2 elemi pont láncok, melyek pontosan egy azonos propozícionális betűt tartalmaznak ellentétes címkével. Jelölje X ezt a propozícionális betűt! Ez esetben, ∆ egy elemi pont lánc ∆1 és ∆2 címkézett elemeiből, kivéve a tX és f X címkézett formulákat.


2013.

7 / 18

Logikai kalkulusok egységes tárgyalása, és alkalmazása az oktatásban A tn-interpretáció mint formális nyelv: 1. pf A1 ˝ f A2 ˝ ¨ ¨ ¨ ˝ f Ak q ñ f pA1 _ A2 _ ¨ ¨ ¨ _ Ak q, ahol k ě 2, 2. pf A1 ` f A2 ` ¨ ¨ ¨ ` f Ak q ñ f pA1 ^ A2 ^ ¨ ¨ ¨ ^ Ak q, ahol k ě 2, 3. tA ñ f A ahol A egy formula. Végeredményképpen, egy f A formula keletkezik, ahol A a tn-interpretáció által generált formula. A fn-interpretáció mint formális nyelv: 1. f A ñ t A ahol A egy formula, 2. ptA1 ˝ tA2 ˝ ¨ ¨ ¨ ˝ tAk q ñ tpA1 ^ A2 ^ ¨ ¨ ¨ ^ Ak q, ahol k ě 2, 3. ptA1 ` tA2 ` ¨ ¨ ¨ ` tAk q ñ tpA1 _ A2 _ ¨ ¨ ¨ _ Ak q, ahol k ě 2. Végeredményképpen, egy tA formula keletkezik, ahol A a fn-interpretáció által generált formula.


2013.

8 / 18


Pont-plusz rezolúció f Z ` pf X ˝ tY q ` pf Y ˝ tZq ` ptX ˝ tZq ` pf X ˝ tZq ` f X ` tX 1. 2. 3. 4. 5. 6. 7.

fZ f X ˝ tY f Y ˝ tZ tX ˝ tZ f X ˝ tZ fX tX

tn-interpretáció 1. Z 2. X _ Y 3. Y _ Z 4. X_ Z 5. X _ Z 6. X 7. X 8. üres klór


1. 2. 3. 4. 5. 6. 7. 8.

2013.

fn-interpretáció Z X ^Y Y ^Z X ^Z X ^Z X X üres duális klóz

(2; 3) (1; 5) (1; 4) (6; 7)

9 / 18


Pont-plusz szekvent

A1 , A2 , ¨ ¨ ¨ , An Ñ B1 , B2 , ¨ ¨ ¨ , Bm

„

A1 _ A2 _ ¨ ¨ ¨ _ An _ B1 _ B2 _ ¨ ¨ ¨ _ Bm Ha eltávolítjuk az átírási algoritmus első szabályát (a cimkézett konjunkciók eltávolítási szabályát), akkor a fenti formula pp-kifejezés alkaja egy pont lánc. Az áttekinthetőség kedvéért feltételezzük hogy Bi (i “ 1, ¨ ¨ ¨ , m) nem tartalmaz diszjunkciót. f A1 _ A2 _ ¨ ¨ ¨ _ An _ B 1 _ B 2 _ ¨ ¨ ¨ _ B m

ñ

tA1 ˝ tA2 ˝ ¨ ¨ ¨ ˝ tAn ˝ f B1 ˝ f B2 ˝ ¨ ¨ ¨ ˝ f Bm Ekkor a fenti pp kifejezés tn-interpretációja egybeesik a szekvent formula alakjával.


2013.

10 / 18


Egy bizonyítás készítése közben több szekventen is dolgozunk párhuzamosan, melyeket most gyűjtsük össze ` jellel elválasztva egy listába. Ekkor az így kapott lista továbbra is pp kifejezés. A pp szekvent kalkulus axiómasémája egy plusz lánc, mely pont láncokból épül fel: f A ˝ tA or γ ˝ f A ˝ tA ahol γ egy pont lánc, A pedíg tetszőleges formula.


2013.

11 / 18


Szekvent kalkulus A pp szekvent kalkulus levezetési szabályai: pf A ˝ γq ` ptB ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk ptA Ą B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk

ptA ˝ f B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk pf A Ą B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk

pf A ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk pt A ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk

ptA ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk pf A ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk

ptA ˝ tB ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk ptA ^ B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk

pf A ˝ γq ` pf B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk pf A ^ B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk

ptA ˝ γq ` ptB ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk ptA _ B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk

pf A ˝ f B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk pf A _ B ˝ γq ` γ1 ` ¨ ¨ ¨ ` γk

ahol γi (i “ 1, ¨ ¨ ¨ , k) egy-egy pont lánc, k ě 0, továbbá γ opcionális pont lánc.


2013.

12 / 18


Az előbbi levezetési szabályok esetében a tn-interpretáció épp a Gentzen-féle szekvent kalkulus levezetési szabályait generálja, következésképp a pp szekvent kalkulus helyes. Példa: 1. f p X Ą 2. t X Ą

p XĄ

Y q Ą pY Ą Xq

Y q Ą pY Ą Xq Y ˝ fY Ą X

3. f X ˝ f Y Ą X ` t Y ˝ f Y Ą X 4. tX ˝ f Y Ą X ` t Y ˝ f Y Ą X 5. tX ˝ f Y Ą X ` f Y ˝ f Y Ą X 6. tX ˝ tY ˝ f X ` f Y ˝ f Y Ą X 7. tX ˝ tY ˝ f X ` f Y ˝ tY ˝ f X


2013.

13 / 18


Az előbbi példa bináris fa reprezentációja:

tX ◦ tY ◦ f X

f Y ◦ tY ◦ f X

tX ◦ f Y ⊃ X

fY ◦ fY ⊃ X

f ¬X ◦ tY ⊃ X

t¬Y ◦ f Y ⊃ X

t¬X ⊃ ¬Y ◦ f Y ⊃ X f (¬X ⊃ ¬Y ) ⊃ (Y ⊃ X)


2013.

14 / 18


Tabló kalkulus • A redukált (konjunkció eltávolítás nélküli) átírási szabály és a tn-interpretáció lehetőséget adott arra, hogy pp szekvent kalkulus levezetések segítségével generáljunk szekventkalkulusbéli levezetést, • a pp-rezolúció esetén az fn-interpretáció duális kalkulust generált, • most pedig a pp szekvent kalkulus fn-interpretációja segítségével a tabló módszerhez jutunk:

f A ` tB tA Ą B

ñ

f A; tB tA Ą B


tA ˝ f B fA Ą B

2013.

ñ

tA fB fA Ą B

...

15 / 18


A pp szekvent kalkulus levezetésének miden lépése a tabló megoldatlan jelölt formuláit gyűjti össze. Az egyes ágakat ` választja el, míg a megoldatlan jelölt formulákat ˝ szeparálja. f (¬X ⊃ ¬Y ) ⊃ (Y ⊃ X) t¬X ⊃ ¬Y fY ⊃ X f ¬X

t¬Y

tX

fY

tY

tY

fX

fX


2013.

16 / 18


Hivatkozások Dragálin, A. G., On a self-dual notation in automated reasoning, Technical Report No 96/16, Debrecen, 1996. Toelstra, A. S. and Schwichtenberg, H., Basic Proof Theory, Cambridge University Press, Cambridge, 1996. Fitting, M., First-order logic and automated theorem proving, Springer, 1996. Stachniak, Z., Resolution Proof Systems: An Algebraic Theory, Kluwer Academic Publishers, York University, North York, Canada, 1996. Pásztor Varga, K. and Várterész, M., A generalized approach to the theorem proving methods in Proc. of 5th International Conference on Applied Informatics, pp. 191-200, Eger, 2001. Pásztor Varga, K. and Várterész, M., Comparison and Usability of two Rewriting Systems for Theorem Proving, Pure Mathematics and Applications, Volume 13, No. 1-2, pp. 293-302, Budapest-Siena, 2002.


2013.

17 / 18


Köszönöm a figyelmet!

Kádek Tamás web.: www.inf.unideb.hu/~kadek email.: [email protected] tel.: 36 52 512 900 / 75230


2013.

18 / 18

Logikai kalkulusok egységes tárgyalása, és alkalmazása az oktatásban

Recommend Documents