Programare nonimperativa

1 Sintaxa limbajului

Vocabularul limbajului este V [ L [ S; unde

Limbajele de primul ordin au fost introduse de Frege ^³n 1879. Com-

parativ cu limbajul calculului cu propozit»ii, structura unui limbaj de primul

ordin este mult mai complex¸a »si ofer¸a un cadru su¯cient pentru reprezentarea

unei clase relativ largi de propozit»ii dintr-un limbaj natural. ^In contextul sis-

temelor bazate pe cuno»stint»e, un limbaj de primul ordin este un sistem formal

ata»sat unui astfel de sistem »si permite proiectarea, analiza »si controlul mecan-

ismelor inferent»iale ^³n gestiunea cuno»stint»elor stocate ^³n baza de cuno»stint»e

a sistemului. Convent»ional, sistemul bazat pe cuno»stint»e modelat prin in-

termediul unui anume limbaj de primul ordin, este referit ca interpretare

intent»ionat¸a pentru acel limbaj. ^In cadrul acestui capitol sunt prezentate

sintaxa »si semantica unui limbaj de primul ordin, reprezent¸ari normalizate

pentru formulele limbajului, modele Herbrand »si metode de demonstrare au-

tomat¸a bazate pe principiul rezolut»iei.

2 Sintaxa limbajelor de primul ordin

Vocabularul V al unui limbaj de primul ordin cont»ine dou¸a tipuri de sim-

boluri »si anume simbolurile logice »si simbolurile non-logice. Spre deosebire

de simbolurile logice, care sunt comune tuturor limbajelor din aceast¸a clas¸a,

simbolurile non-logice sunt de¯nite ^³n funct»ie de interpretarea intent»ionat¸a

pentru limbajul respectiv. De¯nirea mult»imilor de simboluri non-logice pen-

tru construirea unui limbaj de primul ordin aferent unui sistem de cuno»stint»e

dat se nume»ste conceptualizare a sistemului.

Simbolurile logice sunt elementele mult»imii V [ L [ S [ Q; unde:

V este mult»imea variabilelor; V 6= ;.

L = f^;_;!;$; kg este mult»imea conectivelor logice: conjunct»ie, disjunct»ie,

implicat»ie, echivalent»¸a »si negat»ie.

S = f(; )g este mult»imea simbolurilor de punctuat»ie.

Q = f8; 9g este mult»imea cuanti¯catorilor; simbolul 8 este cuanti¯catorul

universal, respectiv simbolul 9 este cuanti¯catorul existent»ial.

Simbolurile non-logice sunt elementele mult»imii CS [ FS [ PS unde:

CS este mult»imea constantelor.

FS este mult»imea simbolurilor functoriale. Fiecare functor f 2 FS este

caracterizat de un num¸ar natural r (f) ¸ 1 numit aritatea functorului

f:

PS este mult»imea simbolurilor predicat»ionale. Fiecare predicat

¼ 2 PS este caracterizat de un num¸ar natural r (¼) ¸ 0 numit aritatea

predicatului ¼:

Presupunem c¸a mult»imile V; L; S; Q;CS; FS; PS sunt dou¸a c^ate dou¸a dis-

juncte.

Vocabularul limbajului este V = V [ L [ S [Q[ CS [ FS [ PS; elementele

mult»imii A = V¤

se numesc asamblaje.

Pentru ® 2 A »si x 2 V; indic¸am prin ® hxi faptul c¸a simbolul x apare cel

put»in o dat¸a printre simbolurile asamblajului ®; respectiv prin ® ixh situat»ia

contrar¸a.

^Intr-un limbaj de prim ordin identi¯c¸am dou¸a mult»imi de structuri simbo-

lice de interes »si anume mult»imea termenilor TERM »si mult»imea formulelor

FORM.

De¯nit»ia 2:1:1 Secvent»a de asamblaje t1; :::; tn este o secvent»¸a generativ¸a

termeni (SGT), dac¸a pentru orice i; 1 · i · n; ti ^³ndepline»ste una din

condit»iile:

¶) ti 2 V [ CS

¶¶) exist¸a f 2 FS »si exist¸a indicii j1; :::; jr(f) cu 1 · jp < i ,

p = 1; :::; r (f) astfel ^³nc^at ti = ftj1 tj2 ::: tjr(f)

De¯nit»ia 2:1:2 Numim termen orice asamblaj t cu proprietatea c¸a exist¸a

n = 1 »si t1; :::; tn¡ SGT; astfel ^³nc^at tn = t: Mult»imea termenilor este notat¸a

TERM:

Observat»ie Dac¸a t1; :::; tn este SGT; atunci t1 2 V [ CS »si

ti 2 TERM; i = 1; :::; n: ^In particular rezult¸a V [ CS ½ TERM.

Observat»ie Gramatica BNF care genereaz¸a limbajul teremenilor este:

hargumenti ! x pentru orice x 2 V

hargumenti ! c pentru orice c 2 CS

hfunctori ! f pentru orice f 2 FS

hlista argumentei ! hargumenti hlista argumentei

htermeni ! hargumenti j hfunctori hlista argumentei

^³mpreun¸a cu regula suplimentar¸a ca num¸arul de termeni din lista de argu-

mente s¸a ¯e egal cu aritatea simbolului functorial respectiv.

Reprezentarea convent»ional¸a a structurilor simbolice termeni este prin

intermediul arborilor de structur¸a.

De¯nit»ia 2:1:3 Arborele T direct»ionat, cu r¸ad¸acin¸a »si v^arfurile etichetate

cu simboluri din mult»imea V [CS [FS este un arbore de structur¸a termen,

dac¸a pentru orice v^arf n al arborelui,

¶) dac¸a od (n) = 0; atunci ' (n) 2 V [ CS

¶¶) dac¸a od (n) ¸ 1; atunci ' (n) 2 FS »si r (' (n)) = od (n)

unde ' (n) este eticheta v^arfului n.

Construct»ia unui arbore de structur¸a T (t) pentru reprezentarea termenu-

lui t 2 TERM poate ¯ realizat¸a recursiv astfel:

a) dac¸a t 2 V [ CS; atunci T (t) = (frg ; ;) »si ' (r) = t

b) dac¸a t = ft1:::tr(f) pentru anume f 2 FS atunci