Złożoność prostych logik domniemań

Na podstawie pracy: Henry Kautz and Bart Selman, Hard Problems for Simple Default Logics. Artificial Intelligence 49 (1991) 243–279.

Rozważać będziemy trzy problemy:

1. znajdowanie rozszerzenia;

2. stwierdzenie czy dana formuła rachunku zdań zachodzi w jakims rozszerzeniu;

3. stwierdzenie czy dana formuła rachunku zdań zachodzi we wszytskich rozszerzeniach;

Założenia:

1. Zbiór aksjomatów A jest koniunkcją literałów.

2. Warunek wstępny, uzasadnienie i konsekwencja są także koniunkcją literałów.

Taką teorię nazywamy disjunction-free (w skrócie D-F).

Klasy teorii:

Unary  p : q/q; p : q ∧ ¬r/p; p : ¬q/¬q;
D-F ordered  a_{1} ∧ … ∧ a_{l} : b_{1} ∧ … ∧ b_{m} ∧ c_{1} ∧ … ∧ c_{n}/b_{1} ∧ … ∧ b_{m}

i dla żadnego literału x nie zachodzi x ≪ x

Ordered unary p : q/q; p : q ∧ ¬r/p; p : ¬q/¬q;

i dla żadnego literału x nie zachodzi x ≪ x

D-F normal  a_{1} ∧ … ∧ a_{l} : b_{1} ∧ … ∧ b_{m}/b_{1} ∧ … ∧ b_{m}
Horn  p_{1} ∧ … ∧ p_{n} : q/q; p_{1} ∧ … ∧ p_{n} : ¬q/¬q
Normal unary  p_{:}q/q; p : ¬q/¬q

Relacja ≪ jest relacją “ostrego” porządku, a relacja ≪ jest relacją porządku oraz

∀δ ∈ D, ∀a ∈ pre(δ), ∀c ∈ just^{∗}(δ), ∀b ∈ concl(δ) a≪b, ¬c ≪ b • Unary – warunek wstępny jest symbolem zdaniowym, a

konsekwecja literałem. Jesli konsekwencja jest literałem pozytywnym, to uzasadnienie może zawierać dodatkowy literał negatywny, wp. jest symbolem zdaniowym.

• D-F ordered – uporządkowanie w sensie relacji ≪ i ≪ – , bez cykli.

• Ordered unary

• D-F normal – teorie normalne D-F.

• Horn – wszystkie literały w warunku wstępnym są pozytywne, a uzasadnienie i konsekwencja są tym samym literałem.

• Normal unary – przecięcie wszystkich wyżej wymienionych.

5