Wykład 1

Zagadnienia podstawowe  dotyczące metod formalnych w informatyce

v   Logika

Analiza języka i czynności badawczych (np. rozumowanie, definiowanie, klasyfikowanie) w celu poznania takich reguł posługiwania się językiem i wykonywania owych czynności, które uczyniłyby tę działalność możliwie najbardziej skuteczną.

v   Logika formalna

Schematy rozumowań niezawodnych

prawdziwe przesłanki    ®        prawdziwe wnioski

v   Podział logiki formalnej:

·     logika tradycyjna

·     współczesna

v   Logika współczesna obejmuje:

·     rachunek zdań

·     rachunek kwantyfikatorów

·     wraz z symbolem identyczności i symbolami funkcyjnymi

·     zawiera wszystkie tautologie logiczne.

v     Teoria mnogości: pozostaje w bliskim związku z logiką. Ta część teorii, która da się sformułować w terminach logicznych, obejmuje algebrę zbiorów Bool’a.

v   Jedyna nauka wcześniejsza – logika. Stanowi ona podstawę do budowania innych nauk

v  Logika w informatyce umożliwia między innymi:

·     badanie własności języków programowania

·     badanie oprogramowania

·     badanie własności metodologii tworzenia oprogramowania

·     specyfikację poszczególnych produktów tworzonych w kolejnych etapach tworzenia oprogramowania

·     programowanie.

1.1. Rachunek zdań

Zdania logiczne i formuły

Przykład 1.1

stała logiczna zw. funktorem zdaniotwórczym

treść podstawiona pod zmienną zdaniową p

treść podstawiona pod zmienną zdaniową p

(1)  „Jabłko jest owocem lub nieprawda, że jabłko jest owocem”- zdanie prawdziwe

treść podstawiona pod zmienną zdaniową (niepodzielna część zdania) p

(2) „Jabłko jest owocem” - zdanie prawdziwe

Zdanie (2) można przekształcić zawsze w zdanie fałszywe:

„Jabłko jest warzywem”                                                         zdanie fałszywe

„Kwiat jest owocem”                                                        zdanie fałszywe

Zdanie (1) jest zawsze prawdziwe

„Kwiat jest owocem” lub nieprawda , że kwiat jest owocem”

Zdanie (1) to  formuła  zw. prawem wyłączonego środka

stała logiczna zw. funktorem zdaniotwórczym

zmienną zdaniową p

zmienną zdaniową p

p lub nie p

(p Ú Ø p)

Formuła generująca zawsze zdania prawdziwe po podstawieniu za zmienną zdaniową(nazwową) określonej treści nazywa się prawem logicznym.

Przykład 1.2

v   „Jeśli (jest tak, że) jeśli grzmi, to błyska, to jeśli nie błyska, to nie grzmi”

v   jeśli (jeśli p to q) to (jeśli nie q to nie p)

v   (p®q) ® (Ø q® Ø p)                                                          formuła zw. prawem transpozycji

Symbole stałe rachunku zdań (symbole funktorów zdaniotwórczych):

Rachunek zdań jest dwuwartościowy:

·       logiczna prawda oznacza 1 (true)

·       logiczny fałsz oznacza 0 (false)

Język rachunku zdań

v   Alfabet rachunku zdań:

1)   symbole stałe logiczne: 1(true), 0(false)

2)   symbole zmiennych zdaniowych: p,q,r,....

3)   symbole spójników logicznych: Ø,Ù,Ú,®,«

4)   symbole pomocnicze: lewy nawias (  oraz prawy nawias ).

v   Zasady budowania formuł

Formuły poprawnie zbudowane, czyli wyrażenia sensowne tego rachunku są:

1)   wyrażenia proste: zmienne zdaniowe p,q,r...

2)   wyrażenia złożone:

a)      jeśli j jest wyrażeniem sensownym, to Øj jest wyrażeniem sensownym

b)     jeśli j jest wyrażeniem sensownym i y jest wyrażeniem sensownym, to wyrażenia jÙy,  jÚy, j®y, jºy są także wyrażeniami sensownym

3)   tylko formuły 1) i 2) są sensowne

4) jeśli formuła j posiada zmienną zdaniową p, a  y jest inną formułą, to przez zastąpienie każdego wystąpienia p formułą y otrzymujemy formułę oznaczoną

                                                           j[y/p].

Przykład 1.3

v  Wyrażenia sensowne:                                           p ®(qÙr) ,               (qÚp)Ùr,

v   Wyrażenia sensowne po zastąpieniu:               (pÚØp)®(qÙr),              ((pÚØp)Úp)Ùr,             

v  Wyrażenia, które nie są sensowne:                p Ør, p Ù(Úq)

Tabela funktorów zdaniotwórczych (istniejących i możliwych do zdefiniowania):

·       funktory jednoargumentowe (dane tabeli są wartościami wyrażeń np. Ø1)