Lógica computacional desde el punto de vista de la programación funcional : eliminación de cuantificadores

TRABAJO FIN DE GRADO FACULTAD DE MATEM´ ATICAS DEPARTAMENTO DE CIENCIAS DE LA COMPUTACI´ ON E INTELIGENCIA ARTIFICIAL L´ OGICA COMPUTACIONAL DESDE EL PUNTO DE VISTA DE LA PROGRAMACI ´ ON FUNCIONAL: ELIMINACI ´ ON DE CUANTIFICADORES Realizado por: Mar´ıa Dolores Mateo Ceballos Supervisado por: D. Jos´e Antonio Alonso Jim´enez Da. Mar´ıa Jos´e Hidalgo Doblado ´ Indice general 1. Introducci´on 7 2. Introducci´on a Ocaml 11 2.1. Definir expresiones y funciones . . . . . . . . . . . . . . . . . . . . . 11 2.2. TiposenOcaml............................. 14 2.3. Funciones predefinidas . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.4. Ficheros de archivos . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3. L´ogica proposicional 17 3.1. Sintaxis de la l´ogica proposicional . . . . . . . . . . . . . . . . . . . 17 3.1.1. Operaciones sint´acticas . . . . . . . . . . . . . . . . . . . . . 19 3.2. Sem´antica de la l´ogica proposicional . . . . . . . . . . . . . . . . . . 20 3.2.1. Escritura de las tablas de verdad . . . . . . . . . . . . . . . 21 3.3. Validez, satisfacibilidad y tautolog´ıas . . . . . . . . . . . . . . . . . 23 3.4. Simplificaci´on y forma normal negativa . . . . . . . . . . . . . . . . 24 3.5. Formas normales disyuntivas y conjuntivas . . . . . . . . . . . . . . 27 3.5.1. Forma normal conjuntiva usando abreviaciones . . . . . . . . 31 3.6. El procedimiento Davis-Putnam . . . . . . . . . . . . . . . . . . . . 35 3.6.1. L´ogica de cl´ausulas . . . . . . . . . . . . . . . . . . . . . . . 35 3.6.2. Procedimiento DP . . . . . . . . . . . . . . . . . . . . . . . 38 3.6.3. Procedimiento DPLL . . . . . . . . . . . . . . . . . . . . . . 39 4. L´ogica de primer orden 41 4.1. Sintaxis de la l´ogica de primer orden . . . . . . . . . . . . . . . . . 41 4.2. Sem´antica de la l´ogica de primer orden . . . . . . . . . . . . . . . . 44 4.2.1. Validez y satisfacibilidad . . . . . . . . . . . . . . . . . . . . 47 4.3. Operaciones sint´acticas sobre f´ormulas . . . . . . . . . . . . . . . . 48 4.4. Forma normal prenexa . . . . . . . . . . . . . . . . . . . . . . . . . 50 4.5. FormadeSkolem ............................ 54 4.6. Teorema de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . 57 4.6.1. Cl´ausulas de primer orden . . . . . . . . . . . . . . . . . . . 58 4.6.2. Extensiones de Herbrand . . . . . . . . . . . . . . . . . . . . 58 3 4´ INDICE GENERAL 5. Eliminaci´on de cuantificadores 61 5.1. Teor´ıas de primer orden . . . . . . . . . . . . . . . . . . . . . . . . 61 5.2. Procedimiento de eliminaci´on de cuantificadores . . . . . . . . . . . 62 5.2.1. Reducci´on del alcance de los cuantificadores . . . . . . . . . 63 5.2.2. Funci´on principal . . . . . . . . . . . . . . . . . . . . . . . . 65 5.3. Teor´ıa de los ´ordenes lineales densos . . . . . . . . . . . . . . . . . . 67 5.3.1. Igualdad............................. 68 5.3.2. Eliminaci´on de cuantificadores para DLO . . . . . . . . . . . 68 5.3.3. Ejemplos............................. 70 Bibliograf´ıa 73 A. C´odigo 75 Abstract Computational Logic is a wide interdisciplinary field having its theoretical and practical roots in mathematics, computer science, logic, and artificial intelligence. Computational Logic try to produce efficient and powerful algorithms for deciding the satisfiability of formulas in logical theories. This work is about propositional and first order logic, and its implementation in the functional language Ocaml. In particular, the aim of this work is to explain the quantifier elimination algorithm. As an example, we develop the quantifier elimination algorithm for the Theory of dense linear orders. Quantifier elimination is an algorithm supported by some logical theories. By eliminating quantifiers from a formula, it makes it possible to test its satisfiability in the sense of propositional logic. 5 Cap´ıtulo 1 Introducci´on Seg´un la RAE, “la l´ogica es la ciencia que expone las leyes, modos y formas de las proposiciones en relaci´on con su verdad o falsedad”. Nacida hace m´as de dos milenios en la Antigua Grecia con Arist´oteles y su investigaci´on acerca de los principios del razonamiento v´alido o correcto, la cual se recoge principalmente en ´ Organon, la l´ogica ha estado estrechamente ligada al desarrollo intelectual del ser humano, al desarrollo de otras ciencias al establecer las formas correctas de razonamiento y, en particular, al desarrollo de las matem´aticas. La l´ogica matem´atica propiamente dicha comienza a desarrollarse principalmente en el siglo XIX, gracias a la contribuci´on de George Boole (1815-1864) y Augustus De Morgan (1806-1871). El primero es el creador de la conocida ´ Algebra de Boole, recogida inicialmente en An´alisis Matem´atico de la L´ogica, publicado en 1847, y extendido en 1854 en Investigaci´on sobre las Leyes del Pensamiento. Augustus De Morgan es conocido, entre otros, por formular las llamadas Leyes de De Morgan. Su obra principal en el campo de la l´ogica es L´ogica formal, publicado en 1847. Entre el final del siglo XIX y el comienzo del siglo XX se sientan las bases de la l´ogica matem´atica moderna. Destaca Gottlob Frege (1848-1925), que en su obra Conceptograf´ıa oEscritura conceptual (1879) introduce una nueva sintaxis, en la que destaca la inclusi´on de los llamados cuantificadores. Las inconsistencias de la teor´ıa puestas de manifiesto en su trabajo motivan a Bertrand Russell y Alfred North Whitehead a publicar, entre 1910 y 1913, un conjunto de tres libros llamado Principia mathematica, en un intento de describir un conjunto de axiomas y reglas de inferencia en l´ogica simb´olica a partir de los que se pudieran probar todas las verdades matem´aticas. Este intento termina con los teoremas de incompletitud de G¨odel, publicados en 1931. En esta ´epoca destacan otros grandes matem´aticos como Jaques Herbrand o David Hilbert. Con el desarrollo de los ordenadores a partir de mediados del siglo XX comienza a desarrollarse la l´ogica computacional, en la que se enmarca este trabajo. 7 8CAP´ ITULO 1. INTRODUCCI ´ ON La l´ogica computacional es un campo interdisciplinar con sus ra´ıces te´oricas y pr´acticas en las matem´aticas, la inform´atica, la l´ogica y la inteligencia artificial. El objetivo de este trabajo es estudiar conceptos b´asicos de la l´ogica proposicional y de primer orden, implem´entandolos en un lenguaje de programaci´on funcional. Esta tarea ser´a desarrollada en los cap´ıtulos 3 y 4, basada en el trabajo de J. Harrison [6]. El fin ´ultimo es estudiar el algoritmo de eliminaci´on de cuantificadores, lo que se har´a a lo largo del cap´ıtulo 5, y cuya implementaci´on se basa tambi´en en el trabajo de J. Harrison. Para el desarrollo te´orico nos apoyamos asimismo en los libros de Z. Manna [3], H. B. Enderton [5] y S. M. Srivastava[9]. Para la implementaci´on hemos usado el lenguaje de programaci´on funcional Ocaml [2]. La primera implementaci´on de este lenguaje aparece en 1987 con el nombre de Caml (acr´onimo de Categorical Abstract Machine Language) y se contin´ua desarrollando hasta 1992. Es creado por el INRIA (Institut National de Recherche en Informatique et en Automatique) en Francia. Objetive Caml, conocido actualmente como Ocaml, se comienza a desarrollar en 1996, como una mejora de las anteriores versiones Caml Light y Caml Special Light, y se renombra como OCaml en 2011. Este lenguaje ofrece, entre otros: Inferencia de tipos, lo cual permite definir operaciones sin explicitar el tipo de los argumentos o del resultado. Definiciones de nuevas estructuras de datos y el uso de las definiciones mediante patrones. Manejo de errores y excepciones. Estas facilidades son las que nos han llevado a escoger Ocaml como lenguaje de programaci´on funcional para el desarrollo del presente trabajo. ´ Este consta de un primer cap´ıtulo en el que introduciremos el lenguaje de programaci´on funcional Ocaml. A lo largo de los dos siguientes cap´ıtulo desarrollaremos la l´ogica proposicional y de primer orden, implement´andola a su vez en Ocaml. Expondremos su sintaxis y sem´antica, la transformaci´on de f´ormulas en diferentes formas normales y algunos procedimientos de decisi´on. Para finalizar, enunciaremos el Teorema de Herbrand, dejando as´ı constancia de que no existe ning´un algoritmo para decidir la satisfacibilidad de una f´ormula de primer orden y, por lo tanto, de la importancia de los algoritmos que deciden la satisfacibilidad restringi´endose a conjuntos m´as peque˜nos de f´ormulas. Por ´ultimo, en el cap´ıtulo 5, desarrollaremos uno de estos algoritmos para decidir la satisfacibilidad de las f´ormulas de una teor´ıa de primer orden. Como ejemplo, veremos un algoritmo para la Teor´ıa de los ´ordenes lineales densos. 9 Existen otros trabajos relativos al algoritmo de eliminaci´on de cuantificadores, como el realizado por Amine Chaieb y Tobias Nipkow para la aritm´etica de Presburger [4]. Nosotros podr´ıamos continuar este trabajo implementando en Ocaml dicho algoritmo para esta teor´ıa, o para otras teor´ıas de primer orden. Adjuntos a este trabajo se acompa˜nan los archivos correspondientes a la implementaci´on del mismo: “inicio.ml”, “lpsintax.ml”, “lpsem.ml”, “defcnf.ml”, “dp.ml”, “lpo.ml”, “skolem.ml”, “elcuant.ml”. 16 CAP´ ITULO 2. INTRODUCCI ´ ON A OCAML 2.4. Ficheros de archivos Para cargar un fichero de c´odigo se escribe en la terminal: # use "nombre.ml";; Los ficheros que se usan en este trabajo, ordenados por cap´ıtulos, deben cargarse en el siquiente orden: 1. C´odigo inicial necesario para este trabajo: # use " inicio.ml";; 2. L´ogica proposicional: # use "lpsintax.ml";; # use "lpsem.ml";; # use "defcnf.ml";; # use "dp.ml";; 3. L´ogica de primer orden: # use "lpo.ml";; # use "skolem.ml";; 4. Eliminaci´on de cuantificadores: # use " elcuan.ml";; Cap´ıtulo 3 L´ogica proposicional El objetivo de la l´ogica es el desarrollo de una lenguaje formal, que carezca de ambig¨uedad, para modelar enunciados. La l´ogica proposicional es la forma m´as simple de la l´ogica. Trata sobre la veracidad o falsedad de las proposiciones, esto es, afirmaciones que pueden ser consideradas verdaderas o falsas. 3.1. Sintaxis de la l´ogica proposicional Los elementos b´asicos de la l´ogica proposicional son: los s´ımbolos de verdad >o ’Verdadero’ y ⊥o ’Falso’, que en nuestra implementaci´on en Ocaml ser´an True yFalse, respectivamente; las variable at´omicas o proposicionales, denotadas com´unmente ’p’, ’q’, ’r’...; las conectivas l´ogicas, que pueden tener un argumento, es decir, ser monarias: •la negaci´on ¬:Not, o tener dos argumentos, es decir, ser binarias: •la conjunci´on ∧:And, •la disyunci´on ∨:Or, •la implicaci´on ⇒:Imp, •la doble implicaci´on, equivalencia o bicondicional ⇔:Iff. El conjunto de las f´ormulas proposicionales se define recursivamente como sigue: >y⊥son f´ormulas proposicionales. Las variables proposicionales son f´ormulas proposicionales. 17 18 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL Si FyGson f´ormulas proposicionales, entonces ¬F,F∨G,F∧G,F⇒G yF⇔Gson f´ormulas proposicionales. Los s´ımbolos de verdad y las variables proposicionales se denominan f´ormulas at´omicas o ´atomos. Para implementar esto en Ocaml definimos un nuevo tipo de dato formula: type (’a)formula = False | True | Atom of ’a | Not of (’a)formula | And of (’a)formula * (’a)formula | Or of (’a)formula * (’a)formula | Imp of (’a)formula * (’a)formula | Iff of (’a)formula * (’a)formula | Forall of string * (’a)formula | Exists of string * (’a)formula;; Hemos a˜nadido adem´as los constructores Forall yExists, que completan la definici´on de este tipo en Ocaml pero que no utilizaremos hasta hablar de l´ogica de primer orden. Por el momento obviaremos ambos constructores en las futuras definiciones de funciones. Definimos el tipo de las variables proposicionales: type prop = P of string;; y una funci´on para usar el nombre de las proposiciones, como cadenas: let pname(P s) = s;; Con esto podemos implementar las f´ormulas proposicionales en Ocaml mediante el tipo prop formula. Para escribir las f´ormulas en Ocaml de una manera “agradable” y parecida a la notaci´on seguida en el desarrollo te´orico, hemos usado varias funciones de impresi´on, pero no entraremos en detalles sobre ello. Establezcamos en lo que sigue una norma de precedencia de los operadores l´ogicos: negaci´on, conjunci´on, disyunci´on, implicaci´on y doble implicaci´on. En caso de igualdad, los asociaremos por la derecha. Veamos un ejemplo: # let fm = <<p ==> q <=> r /\ s \/ (t <=> ˜ ˜u /\ v)>>;; val fm : prop formula = <<p ==> q <=> r /\ s \/ (t <=> ˜(˜u) /\ v)>> Formalmente, dicha f´ormula se escribir´ıa: (p⇒q)⇔((r∧s)∨(t⇔(¬(¬u)∧v))) 3.1. SINTAXIS DE LA L ´ OGICA PROPOSICIONAL 19 3.1.1. Operaciones sint´acticas Es conveniente tener operaciones sint´acticas correspondientes a los constructores de formula que podamos usar como funciones de Ocaml. let mk_and p q = And(p,q) and mk_or p q = Or(p,q) and mk_imp p q = Imp(p,q) and mk_iff p q = Iff(p,q) and mk_forall x p = Forall(x,p) and mk_exists x p = Exists(x,p);; Al mismo tiempo, dada una f´ormula, nos gustar´ıa obtener sus componentes seg´un el operador l´ogico principal a las que se le aplica. As´ı tenemos las funciones: let dest_iff fm = match fm with Iff(p,q) -> (p,q) | _ -> failwith "dest_iff";; let dest_and fm = match fm with And(p,q) -> (p,q) | _ -> failwith "dest_and";; let dest_or fm = match fm with Or(p,q) -> (p,q) | _ -> failwith "dest_or";; let dest_imp fm = match fm with Imp(p,q) -> (p,q) | _ -> failwith "dest_imp";; De manera similar, las funciones siguientes descomponen una f´ormula que contiene conjunciones y disyunciones, devolviendo de manera recursiva una lista formada por las f´ormulas proposicionales a las que se aplican dichos operadores: let rec conjuncts fm = match fm with And(p,q) -> conjuncts p @ conjuncts q | _ -> [fm];; let rec disjuncts fm = match fm with Or(p,q) -> disjuncts p @ disjuncts q | _ -> [fm];; Para obtener p y q de una f´ormula p⇒q, es decir, su antecedente y su consecuente, definimos: let antecedent fm = fst(dest_imp fm);; let consequent fm = snd(dest_imp fm);; A veces necesitamos definir funciones por recursi´on sobre f´ormulas. La siguiente aplica una funci´on sobre todos los ´atomos de una f´ormula, pero deja la estructura inalterada. Notemos as´ı que Ocaml admite definiciones de funciones de orden superior. 20 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL let rec onatoms f fm = match fm with Atom a -> f a | Not(p) -> Not(onatoms f p) | And(p,q) -> And(onatoms f p,onatoms f q) | Or(p,q) -> Or(onatoms f p,onatoms f q) | Imp(p,q) -> Imp(onatoms f p,onatoms f q) | Iff(p,q) -> Iff(onatoms f p,onatoms f q) | Forall(x,p) -> Forall(x,onatoms f p) | Exists(x,p) -> Exists(x,onatoms f p) | _ -> fm;; La siguiente itera una funci´on binaria a trav´es de todos los ´atomos de una f´ormula. let rec overatoms f fm b = match fm with Atom(a) -> f a b | Not(p) -> overatoms f p b | And(p,q) | Or(p,q) | Imp(p,q) | Iff(p,q) -> overatoms f p (overatoms f q b) | Forall(x,p) | Exists(x,p) -> overatoms f p b | _ -> b;; Una aplicaci´on de esto podr´ıa ser obtener todos los ´atomos de una f´ormula o, de manera m´as general, iterar una funci´on f sobre el conjunto de todos los ´atomos: let atom_union f fm = setify (overatoms (fun h t -> f(h)@t) fm []);; donde la funci´on setify ordena una lista dada y elimina las repeticiones. 3.2. Sem´antica de la l´ogica proposicional Como las f´ormulas proposicionales representan afirmaciones que pueden ser verdaderas o falsas, el significado de una f´ormula es uno de los dos valores de verdad: ’Verdadero’ y ’Falso’. Sin embargo, al igual que una expresi´on algebraica x+y+1 s´olo tiene un significado definido cuando conocemos lo que representan las variables xey, el significado de una f´ormula proposicional depende de los valores de verdad asignados a sus ´atomos. Esto viene dado por una interpretaci´on, que es una aplicaci´on del conjunto de los ´atomos al conjunto de los valores de verdad ’Verdadero’. ’Falso’. Para representar dichas interpretaciones en Ocaml usaremos funciones que para cada variable proposicional devuelvan true ofalse. Dada una f´ormula fm y una interpretaci´on v, la siguiente funci´on eval´ua el valor de dicha f´ormula fm en la interpretaci´on v: 3.2. SEM ´ ANTICA DE LA L ´ OGICA PROPOSICIONAL 21 let rec eval fm v = match fm with False -> false | True -> true | Atom(x) -> v(x) | Not(p) -> not(eval p v) | And(p,q) -> (eval p v) && (eval q v) | Or(p,q) -> (eval p v) || (eval q v) | Imp(p,q) -> not(eval p v) || (eval q v) | Iff(p,q) -> (eval p v) = (eval q v);; Notemos que en la definici´on de esta funci´on no se han considerado los constructores Forall yExists de la definici´on del tipo de dato formula pues, como ya comentamos, los obviaremos por el momento. Incluyamos una tabla de verdad que muestre como el valor de una f´ormula viene determinado por el de sus subf´ormulas inmediatas. p q ¬p p ∧q p ∨q p ⇒q p ⇔q Falso Falso Verdadero Falso Falso Verdadero Verdadero Falso Verdadero Falso Verdadero Verdadero Falso Verdadero Falso Falso Falso Verdadero Falso Falso Verdadero Verdadero Verdadero Verdadero Verdadero Verdadero Veamos un ejemplo sobre c´omo evaluar la f´ormula p∧q⇒q∨r, si p,qyrtoman los valores ’Verdadero’, ’Falso’ y ’Verdadero’, respectivamente; o ’Verdadero’, ’Verdadero’ y ’Falso’. # eval <<p /\ q ==> q /\ r>> (function P"p" -> true | P"q" -> false | P"r" -> true);; - : bool = true # eval <<p /\ q ==> q /\ r>> (function P"p" -> true | P"q" -> true | P"r" -> false);; - : bool = false 3.2.1. Escritura de las tablas de verdad Como indic´abamos anteriormente, es posible obtener el conjunto de los ´atomos de una f´ormula, lo cual nos servir´a, entre otras cosas, para definir todas las posibles interpretaciones de dicha f´ormula. let atoms fm = atom_union (fun a -> [a]) fm;; Adem´as podemos implementar en Ocaml las tablas de verdad para todos los posibles valores de cada ´atomo. Para ello definimos primero una funci´on onallvalua- 22 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL tions que verifica si otra funci´on subfn devuelve true sobre cada posible interpretaci´on de los ´atomos de ats, usando una interpretaci´on existente vpara todos los dem´as ´atomos. Cada interpretaci´on es construida redefiniendo vsucesivamente para darles a cada ´atomo los valores true yfalse, y llamarlas recursivamente: let rec onallvaluations subfn v ats = match ats with [] -> subfn v | p::ps -> let v’ t q = if q = p then t else v(q) in onallvaluations subfn (v’ false) ps && onallvaluations subfn (v’ true) ps;; Ahora podemos usar esta funci´on para escribir tablas de verdad donde aparezca en cada columna el valor de los ´atomos de la f´ormula y de ´esta, y por filas todas las posibles interpretaciones. let print_truthtable fm = let ats = atoms fm in let width = itlist (max ** String.length ** pname) ats 5 + 1 in let fixw s = sˆString.make(width - String.length s) ’ ’ in let truthstring p = fixw (if p then "true" else "false") in let mk_row v = let lis = map (fun x -> truthstring(v x)) ats and ans = truthstring(eval fm v) in print_string(itlist (ˆ) lis ("| "ˆans)); print_newline(); true in let separator = String.make (width * length ats + 9) ’-’ in print_string(itlist (fun s t -> fixw(pname s) ˆ t) ats "| formula"); print_newline(); print_string separator; print_newline(); let _ = onallvaluations mk_row (fun x -> false) ats in print_string separator; print_newline();; Veamos un ejemplo: # print_truthtable <<p /\ q ==> q /\ r>>;; p q r | formula --------------------------- false false false | true false false true | true false true false | true false true true | true true false false | true true false true | true true true false | false true true true | true --------------------------- - : unit = () 3.3. VALIDEZ, SATISFACIBILIDAD Y TAUTOLOG´ IAS 23 3.3. Validez, satisfacibilidad y tautolog´ıas Decimos que una interpretaci´on satisface una f´ormula Fsi la evaluaci´on de ´esta sobre dicha f´ormula devuelve ’Verdadero’. Esta interpretaci´on se llama modelo de F. Para nuestra implementaci´on en Ocaml esto es eval p v = true, donde pes la f´ormula y ves la interpretaci´on. Una f´ormula se dice que es una tautolog´ıa o una validez l´ogica si es satisfecha por todas las interpretaciones o, equivalentemente, si el valor de su tabla de verdad es ’Verdadero’ en todas las filas. satisfacible si existe alguna interpretaci´on que la satisfaga. Esto es, si el valor de alguna de las filas de su tabla de verdad es ’Verdadero’. insatisfacible si no existe ninguna interpretaci´on que satisfaga la f´ormula o, equivalentemente, si el valor de cada fila de su tabla de verdad es ’Falso’. Notar adem´as que una f´ormula Fes insatisfacible si y s´olo si ¬Fes una tautolog´ıa. Para implementar estos conceptos en Ocaml evaluaremos directamente todas las interpretaciones: let tautology fm = onallvaluations (eval fm) (fun s -> false) (atoms fm);; As´ı la funci´on onallvaluations recorre todas las posibles interpretaciones de la f´ormula fm hasta encontrar una que no la satisfaga, devolviendo false, o devolviendo true si recorre todas las interpretaciones y ´estas la satisfacen. Podemos definir asimismo la satisfacibilidad y la insatisfacibilidad en t´erminos de la funci´on tautology. let unsatisfiable fm = tautology(Not fm);; let satisfiable fm = not(unsatisfiable fm);; A continuaci´on pondremos algunos ejemplos. # tautology <<p \/ ˜p>>;; - : bool = true # tautology <<p /\ ˜p>>;; - : bool = false # unsatisfiable <<p /\ ˜p>>;; - : bool = true # tautology <<p \/ q ==> q \/ (p <=> q)>>;; - : bool = false # satisfiable <<p \/ q ==> q \/ (p <=> q)>>;; - : bool = true 24 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL 3.4. Simplificaci´on y forma normal negativa En l´ogica, las formas normales para las f´ormulas son de gran importancia, y pueden aportar valiosa informaci´on. Las formas normales son f´ormulas l´ogicamente equivalentes a las dadas, con una expresi´on determinada. Pero antes de proceder a crearlas, es conveniente definir ciertas reglas de simplificaci´on. En primer lugar definiremos algunas reglas de simplificaci´on sobre los operadores l´ogicos aplicados a los valores de verdad: ¬> ⇔ ⊥,¬ ⊥ ⇔ > ¬(¬p)⇔p p∧ ⊥ ⇔ ⊥,⊥ ∧ p⇔ ⊥ p∧ > ⇔ p,> ∧ p⇔p p∨ ⊥ ⇔ p,⊥ ∨ p⇔p p∨ > ⇔ >,> ∨ p⇔ > (⊥ ⇒ p)⇔ >, (p⇒ >)⇔ > (> ⇒ p)⇔p, (p⇒ ⊥)⇔ ¬p (p⇔ >)⇔p, (> ⇔ p)⇔p (p⇔ ⊥)⇔ ¬p, (⊥ ⇔ p)⇔ ¬p Podemos implementar en Ocaml dicha simplificaci´on: let psimplify1 fm = match fm with Not False -> True | Not True -> False | Not(Not p) -> p | And(p,False) | And(False,p) -> False | And(p,True) | And(True,p) -> p | Or(p,False) | Or(False,p) -> p | Or(p,True) | Or(True,p) -> True | Imp(False,p) | Imp(p,True) -> True | Imp(True,p) -> p | Imp(p,False) -> Not p | Iff(p,True) | Iff(True,p) -> p | Iff(p,False) | Iff(False,p) -> Not p | _ -> fm;; que podemos aplicar a una f´ormula de manera recursiva: 3.4. SIMPLIFICACI ´ ON Y FORMA NORMAL NEGATIVA 25 let rec psimplify fm = match fm with | Not p -> psimplify1 (Not(psimplify p)) | And(p,q) -> psimplify1 (And(psimplify p,psimplify q)) | Or(p,q) -> psimplify1 (Or(psimplify p,psimplify q)) | Imp(p,q) -> psimplify1 (Imp(psimplify p,psimplify q)) | Iff(p,q) -> psimplify1 (Iff(psimplify p,psimplify q)) | _ -> fm;; Notemos nuevamente que no hemos considerado los constructores Forall y Exists de la definici´on del tipo de dato formula. Veamos un ejemplo de esta simplificaci´on: # psimplify <<(true ==> (x <=> false)) ==> ˜(y \/ false /\ z)>>;; - : prop formula = <<˜x ==> ˜y>> Un literal es un ´atomo o su negaci´on. Decimos que un literal es negativo si es la negaci´on de un ´atomo, y positivo en otro caso. Podemos implementar ambas definiciones en Ocaml suponiendo que las estamos aplicando a un ´atomo. let negative = function (Not p) -> true | _ -> false;; let positive lit = not(negative lit);; Estaremos negando un literal si escribimos ¬psi el literal pes positivo, y eliminaremos la negaci´on si es negativo. let negate = function (Not p) -> p | p -> Not p;; Una f´ormula est´a en forma normal negativa o NNF (del ingl´es, negative normal form) si se construye a partir de literales usando s´olo las conectivas binarias ∧y ∨, y la negaci´on aplicada s´olo a ´atomos, adem´as de si es uno de los casos triviales ⊥o>. Podemos transformar una f´ormula en otra l´ogicamente equivalente en forma normal negativa, eliminando los operadores ⇒y⇔en funci´on de las otras conectivas: p⇒q⇔ ¬ (p∧ ¬q) p⇔q⇔ ¬ (p∧ ¬q)∧ ¬ (¬p∧q) o, lo que es lo mismo, p⇒q⇔ ¬p∨q p⇔q⇔ ¬p∨q∧p∨ ¬q y aplicando las leyes de De Morgan y la ley de la doble negaci´on, las cuales enunciamos a continuaci´on: 32 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL (p∨(q∧ ¬r)) ∧s Introducimos un nuevo ´atomo p1, no usado antes en la f´ormula, para abreviar q∧ ¬r, combinando la f´ormula abreviada con la definici´on de p1: (p1⇔q∧ ¬r)∧(p∨p1)∧s Procedemos ahora de manera an´aloga, introduciendo una variable p2para abreviar p∨p1: (p1⇔q∧ ¬r)∧(p2⇔p∨p1)∧p2∧s yp3como una abreviaci´on de p2∧s: (p1⇔q∧ ¬r)∧(p2⇔p∨p1)∧(p3⇔p2∧s)∧p3 Finalmente transformamos cada una de las f´ormulas de las conjunciones en forma normal conjuntiva usando los m´etodos ya vistos: (¬p1∨q)∧(¬p1∨ ¬r)∧(p1∨ ¬q∨r)∧(¬p2∨p∨p1)∧(p2∨ ¬p)∧(p2∨ ¬p1)∧ (¬p3∨p2)∧(¬p3∨s)∧(p3∨ ¬p2∨ ¬s)∧p3 En el peor caso, el coste de transformaci´on de este nuevo algoritmo no es exponencial, lo cual supone una mejora con respecto al que vimos anteriormente que, en el peor caso, era exponencial. Pasemos a la implementaci´on de este m´etodo en Ocaml. Para las nuevas variables proposicionales, usaremos nombres de la forma pn. La siguiente funci´on devuelve un ´atomo y su ´ındice incrementado en una unidad, listo para usarlo la siguiente vez. let mkprop n = Atom(P("p_"ˆ(string_of_num n))),n +/ Int 1;; donde la funci´on string of num transforma un elemento de tipo num (n´umero) en una cadena. Por simplicidad, supongamos que las f´ormulas de partida han sido presimplificadas mediante la funci´on nenf; as´ı pues las negaciones s´olo son aplicadas a los ´atomos y las implicaciones han sido eliminadas, aunque no los bicondicionales. La funci´on recursiva principal maincnf toma una terna que consiste en la f´ormula que queremos transformar, una funci´on con las abreviaciones hechas hasta el momento, y un contador de los ´ındices de las variables. Devuelve una terna similar con la f´ormula transformada, las definiciones, a˜nadiendo las nuevas, y un nuevo contador de los ´ındices usados. Descomponemos una f´ormula seg´un sus conectivas binarias en las subf´ormulas a las que se les aplican; entonces una funci´on defstep que hace el trabajo principal las toma como argumentos op y(p,q). 3.5. FORMAS NORMALES DISYUNTIVAS Y CONJUNTIVAS 33 let rec maincnf (fm,defs,n as trip) = match fm with And(p,q) -> defstep mk_and (p,q) trip | Or(p,q) -> defstep mk_or (p,q) trip | Iff(p,q) -> defstep mk_iff (p,q) trip | _ -> trip and defstep op (p,q) (fm,defs,n) = let fm1,defs1,n1 = maincnf (p,defs,n) in let fm2,defs2,n2 = maincnf (q,defs1,n1) in let fm’ = op fm1 fm2 in try (fst(apply defs2 fm’),defs2,n2) with Failure _ -> let v,n3 = mkprop n2 in (v,(fm’|->(v,Iff(v,fm’))) defs2,n3);; Notemos que maincnf ydefstep son mutuamente recurrentes. Dentro de defstep, una llamada recursiva a maincnf transforma la subf´ormula izquierda p, devolviendo la f´ormula transformada fm1, una lista aumentada de definiciones defs1 y un contador n1. La subf´ormula derecha qjunto con la nueva lista de definiciones y el contador son usados en otra llamada recursiva, devolviendo una f´ormula transformada fm2, nuevas definiciones defs2 y un contador n2. Entonces construimos la f´ormula fm’, aplicando el constructor op que nos proporcion´o maincnf al principio a las f´ormulas fm1 yfm2. A continuaci´on verificamos si ya hay una definici´on correspondiente a esta f´ormula; si es as´ı, devolvemos la variable que define. En otro caso, creamos una nueva variable ve insertamos una nueva definici´on, devolviendo finalmente dicha variable y el nuevo contador despu´es de la llamada a mkprop. Necesitamos estar seguros de que ninguno de nuestros nuevos ´atomos introducidos ya han aparecido en la f´ormula de partida. Esto lo conseguiremos gracias a la funci´on siguiente: let max_varindex pfx = let m = String.length pfx in fun s n -> let l = String.length s in if l <= m or String.sub s 0 m <> pfx then n else let s’ = String.sub s m (l - m) in if forall numeric (explode s’) then max_num n (num_of_string s’) else n;; Ahora podemos implementar la funci´on principal. Primero simplificamos la f´ormula, obteniendo fm’, y usamos esta f´ormula para elegir un ´ındice de variable de partida apropiado, a˜nadiendo 1 al mayor n para el que ya existe una variable p n. Entonces llamamos a la funci´on principal, que mantenemos como un par´ametro fn para posibles modificaciones futuras, empezando sin abreviaciones o definiciones 34 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL y con el ´ındice inicial como contador. Devolvemos la forma normal conjuntiva resultante representada como conjunto de conjuntos: let mk_defcnf fn fm = let fm’ = nenf fm in let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm’ (Int 0) in let (fm’’,defs,_) = fn (fm’,undefined,n) in let deflist = map (snd ** snd) (graph defs) in unions(simpcnf fm’’ :: map simpcnf deflist);; Por ´ultimo, para transformar la lista de listas que devuelve mk defncf en la f´ormula equivalente, se define: let defcnf fm = list_conj(map list_disj(mk_defcnf maincnf fm));; Ve´amoslo en el ejemplo que usamos al principio para explicar la transformaci´on: # defcnf <<(p \/ (q /\ ˜r)) /\ s>>;; - : prop formula = <<(p \/ p_1 \/ ˜p_2) /\ (p_1 \/ r \/ ˜q) /\ (p_2 \/ ˜p) /\ (p_2 \/ ˜p_1) /\ (p_2 \/ ˜p_3) /\ p_3 /\ (p_3 \/ ˜p_2 \/ ˜s) /\ (q \/ ˜p_1) /\ (s \/ ˜p_3) /\ (˜p_1 \/ ˜r)>> Sin embargo, podemos optimizar el procedimiento evitando algunas definiciones redundantes. En primer lugar, cuando la f´ormula inicial se trata de conjunciones iteradas, podemos pasar cada subf´ormula inmediata a forma normal conjuntiva separadamente y unirlas despu´es. Si adem´as estas subf´ormulas contienen disyunciones podemos seguir descendiendo a trav´es de ellas sin introducir nuevas definiciones o abreviaciones. Para codificarlo, primero descendemos a trav´es de conjunciones y disyunciones anidadas, antes de empezar a introducir variables de definici´on. La siguiente funci´on subcnf tiene la misma estructura que defstep pero no introduce nuevas definiciones, y tiene un par´ametro adicional sfn: let subcnf sfn op (p,q) (fm,defs,n) = let fm1,defs1,n1 = sfn(p,defs,n) in let fm2,defs2,n2 = sfn(q,defs1,n1) in (op fm1 fm2,defs2,n2);; Usamos la funci´on anterior primero para definir una funci´on que descienda recursivamente a trav´es de las disyunciones para transformar las subf´ormulas inmediatas: 3.6. EL PROCEDIMIENTO DAVIS-PUTNAM 35 let rec orcnf (fm,defs,n as trip) = match fm with Or(p,q) -> subcnf orcnf mk_or (p,q) trip | _ -> maincnf trip;; y a su vez para definir una funci´on que descienda recursivamente a trav´es de las conjunciones llamando a la funci´on orcnf: let rec andcnf (fm,defs,n as trip) = match fm with And(p,q) -> subcnf andcnf mk_and (p,q) trip | _ -> orcnf trip;; Ahora la funci´on principal es la misma excepto que se usa andcnf en lugar de maincnf. Definimos a continuaci´on dos funciones: la primera devuelve el resultado representado como una lista de listas, mientras que la segunda lo hace representado como una f´ormula: let defcnfs fm = mk_defcnf andcnf fm;; let defcnf fm = list_conj (map list_disj (defcnfs fm));; Veamos un ejemplo: # defcnf <<(p \/ (q /\ ˜r)) /\ s>>;; - : prop formula = <<(p \/ p_1) /\ (p_1 \/ r \/ ˜q) /\ (q \/ ˜p_1) /\ s /\ (˜p_1 \/ ˜r)>> 3.6. El procedimiento Davis-Putnam El procedimiento Davis-Putnam es un m´etodo para decidir la satisfacibilidad de una f´ormula proposicional en forma clausal. Actualmente hay dos algoritmos diferentes, llamados com´unmente ’Davis-Putnam’. El algoritmo original se denomina ’Davis-Putnam’ (DP), y el segundo algoritmo, que es una variante de ´este presentada m´as tarde, se denomina ’Davis-Putnam-Loveland-Logemann’ (DPLL). Hablaremos primero del algoritmo DP. 3.6.1. L´ogica de cl´ausulas Una cl´ausula es un conjunto finito de literales {L1, ..., Ln}. Lo denotaremos generalmente por C. Denotaremos a los conjuntos de cl´ausulas por S. Diremos que una interpretaci´on Ies modelo de una cl´ausula Csi es modelo de alguno de sus literales. Lo notaremos I|=C. Por tanto C={L1, ..., Ln}es 36 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL equivalente a la f´ormula F=L1∨... ∨Ln, pues I(C) = I(F) para cualquier interpretaci´on I. Diremos que una interpretaci´on Ies modelo de un conjunto de cl´ausulas Ssi es modelo de todas sus cl´ausulas. Lo notaremos I|=S. Por tanto: S={{L1,1, ..., L1,k1}, ..., {Lm,1, ..., Lm,km}} es equivalente a la f´ormula F= (L1,1∨... ∨L1,k1)∧... ∧(Lm,1∨... ∨Lm,km). Ya hemos visto que toda f´ormula se puede escribir como una conjunci´on de disyunciones, es decir, en forma normal conjuntiva. Por tanto, toda f´ormula Fes equivalente a un conjunto de cl´ausulas, lo cual se denomina la forma de clausal de F. Un conjunto de cl´ausulas es consistente si tiene alg´un modelo, e inconsistente si no lo tiene. La cl´ausula vac´ıa, denotada , no tiene modelos. Por tanto, todo conjunto conteniendo la cl´ausula vac´ıa es inconsistente. Sin embargo, como toda interpretaci´on es modelo del conjunto vac´ıo de cl´ausulas, ´este es consistente. En Ocaml representaremos las cl´ausulas por listas y los conjuntos de cl´ausulas como listas de listas. Los casos triviales, es decir, el conjunto vac´ıo de cl´ausulas y el conjunto conteniendo la cl´ausula vac´ıa ser´an representados por la lista vac´ıa y la lista conteniendo una lista vac´ıa, respectivamente. El procedimiento Davis-Putnam se aplica a un conjunto de cl´ausulas S, transform´andolo hasta obtener: ∈S, en cuyo caso Ses inconsistente. S=∅, en cuyo caso Ses consistente. En el primer caso la f´ormula cuya forma clausal es Ses insatisfacible, mientras que en el segundo es satisfacible. Hay tres transformaciones b´asicas que preservan la satisfacibilidad usadas en el procedimiento DP: Regla de eliminaci´on unitaria. Regla de eliminaci´on de literales puros. Regla de resoluci´on proposicional. Las dos primeras reglas hacen el conjunto de cl´ausulas m´as simple, reduciendo el n´umero total de literales. Por ello aplicamos estas reglas tanto como nos sea posible. La tercera regla es aplicada s´olo cuando no se pueden aplicar las anteriores, pues incrementa el tama˜no de la forma clausal. Regla de eliminaci´on unitaria. Esta regla puede ser aplicada si existe una cl´ausula unidad, esto es, una cl´ausula conteniendo un ´unico literal. En ese caso, dicho literal debe ser cierto para que lo sea el conjunto de cl´ausulas. Esta regla consiste en eliminar todas las cl´ausulas que 3.6. EL PROCEDIMIENTO DAVIS-PUTNAM 37 contienen el literal, incluyendo la cl´ausula unidad, y eliminar de todas las dem´as cl´ausulas la negaci´on de dicho literal. Para implementarlo como una lista de listas, una cl´ausula unidad ser´a una lista de longitud 1. let one_literal_rule clauses = let u = hd (find (fun cl -> length cl = 1) clauses) in let u’ = negate u in let clauses1 = filter (fun cl -> not (mem u cl)) clauses in image (fun cl -> subtract cl [u’]) clauses1;; Si no hay ninguna cl´ausula unidad, dicha funci´on devolver´a una excepci´on. Esto hace f´acil aplicarla repetidamente hasta que no haya m´as cl´ausulas unidad. Regla de eliminaci´on de literales puros. Esta regla se basa en el hecho de que si un literal ocurre s´olo positivamente o s´olo negativamente en el conjunto de todas las cl´ausulas, podemos eliminar dichas cl´ausulas preservando la satisfacibilidad. A estos literales los llamamos literales puros. Para implementar esta regla comenzamos tomando el conjunto de todos los literales que aparecen en el conjunto de cl´ausulas. Hacemos una partici´on de dicho conjunto en los literales positivos y negativos, obteniendo a continuaci´on los literales puros, y eliminando todas las cl´ausulas que contienen alguno de ellos. let affirmative_negative_rule clauses = let neg’,pos = partition negative (unions clauses) in let neg = image negate neg’ in let pos_only = subtract pos neg and neg_only = subtract neg pos in let pure = union pos_only (image negate neg_only) in if pure = [] then failwith "affirmative_negative_rule" else filter (fun cl -> intersect cl pure = []) clauses;; Nuevamente esta funci´on devuelve un fallo si no existen literales puros. Regla de resoluci´on proposicional. Esta regla es la ´unica que incrementa el tama˜no de la f´ormula. Sin embargo, elimina completamente cualquier ´atomo sin ning´un requerimiento especial de las cl´ausulas que lo contienen. Se aplica cuando un literal ocurre positivamente en alguna cl´ausula y negativamente en otra distinta. Tengamos en cuenta que si hemos eliminado previamente las tautolog´ıas y los literales puros, cualquier literal tendr´a esta propiedad. Sea Sun conjunto de cl´ausulas, y pun literal en las condiciones anteriores. Podemos escribir Scomo S={{p}∪Ci|1≤i≤m}∪{{¬p}∪Dj|1≤j≤n}∪S0, donde CiyDjson conjuntos de literales en los que no aparecen p,¬p; y S0es un conjunto de cl´ausulas para las que ocurre lo mismo. Sea Iuna interpretaci´on tal que I|=S. As´ı, si pes cierto en Itambi´en deben de serlo todos los Dj, y s´ı lo es ¬plo ser´an a su vez todos los Ci. En cualquiera 38 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL caso, Ci∪Djse verificar´a en dicha interpretaci´on. Por tanto, podemos transformar Sen el conjunto de cl´ausulas S0={Ci∪Dj|1≤i≤m, 1≤j≤n} ∪ S0. Rec´ıprocamente, sea I0una interpretaci´on tal que I0|=S0. Si existe un Ckque no sea cierto en ella, deben ser ciertos todos los Dj, pues Ck∪Djs´ı debe verificarse, y podr´ıamos tomar pverdadero en dicha interpretaci´on, para la que Sse satisfar´ıa. El razonamiento es an´alogo si alg´un Dlno es cierto. Por tanto, esta regla mantiene la equisatisfacibilidad. Llamaremos a la cl´ausula Ci∪Djla resolvente de {p} ∪ Ciy{¬p} ∪ Dj, y diremos que se ha obtenido por resoluci´on o, m´as concretamente, por resoluci´on en p. Implementemos este proceso en Ocaml: let resolve_on p clauses = let p’ = negate p and pos,notpos = partition (mem p) clauses in let neg,other = partition (mem p’) notpos in let pos’ = image (filter (fun l -> l <> p)) pos and neg’ = image (filter (fun l -> l <> p’)) neg in let res0 = allpairs union pos’ neg’ in union other (filter (non trivial) res0);; Para aplicar esta regla, debemos decidir respecto de qu´e literal vamos a hacer la resoluci´on. Dado un literal l, podemos predecir el cambio en el n´umero de cl´ausulas resultantes de la resoluci´on en l: let resolution_blowup cls l = let m = length(filter (mem l) cls) and n = length(filter (mem (negate l)) cls) in m * n - m - n;; Resolveremos respecto del literal que minimice esta funci´on. let resolution_rule clauses = let pvs = filter positive (unions clauses) in let p = minimize (resolution_blowup clauses) pvs in resolve_on p clauses;; 3.6.2. Procedimiento DP Definiremos este proceso de manera recursiva. Intentaremos aplicar sucesivamente y en este orden las reglas de eliminaci´on unitaria, de eliminaci´on de literales puros y de resoluci´on proposicional con cada nuevo conjunto de cl´ausulas que obtengamos, hasta obtener la lista vac´ıa, en cuyo caso devolveremos true, o la lista conteniendo la lista vac´ıa, devolviendo false. Esta recursi´on debe terminar, pues con cada regla reducimos el n´umero de ´atomos distintos y, con las dos primeras, tambi´en el de cl´ausulas. 3.6. EL PROCEDIMIENTO DAVIS-PUTNAM 39 let rec dp clauses = if clauses = [] then true else if mem [] clauses then false else try dp (one_literal_rule clauses) with Failure _ -> try dp (affirmative_negative_rule clauses) with Failure _ -> dp(resolution_rule clauses);; Podemos usar este procedimiento para determinar la satisfacibilidad de una f´ormula. Tambi´en podemos determinar su validez a trav´es de la negaci´on de dicha f´ormula. let dpsat fm = dp(defcnfs fm);; let dptaut fm = not(dpsat(Not fm));; Por ejemplo: # tautology <<(p \/ (q /\ ˜r)) /\ s>>;; - : bool = false # dptaut <<(p \/ (q /\ ˜r)) /\ s>>;; - : bool = false 3.6.3. Procedimiento DPLL Para problemas m´as dif´ıciles, el n´umero y tama˜no de las cl´ausulas generadas en el procedimiento DP puede crecer enormemente. Es esto lo que motiv´o a Davis, Logemann y Loveland a reemplazar la regla de resoluci´on por una regla de divisi´on. Si ninguna de las dos primeras reglas vistas anteriormente son aplicables, entonces podemos elegir un literal p, y la consistencia de un conjunto de cl´ausulas Sse reduce a decidir la consistencia de S∪ {p}o de S∪ {¬p}. As´ı, si S∪ {p}es consistente, existir´ıa una interpretaci´on en la que pser´ıa verdadero y que tambi´en ser´ıa modelo de S. Si fuera consistente S∪ {¬p}, deber´ıa existir una interpretaci´on que fuera modelo de Sy en la que pfuera falso. Tras aplicar esta regla, podr´ıamos aplicar seguidamente la regla de eliminaci´on unitaria, que reducir´ıa el conjunto de cl´ausulas. Es por ello que tenemos garantizada la finalizaci´on de este procedimiento. An´alogamente al procedimiento DP, debemos elegir con qu´e literal aplicaremos la regla de divisi´on. Parece sensato escoger aquel que aparece m´as veces, tanto positiva como negativamente, pues la posterior aplicaci´on de la regla de eliminaci´on unitaria provocar´ıa una mayor simplificaci´on. Definimos as´ı un contador del n´umero de veces que aparece cada literal en un conjunto de cl´ausulas: let posneg_count cls l = let m = length(filter (mem l) cls) and n = length(filter (mem (negate l)) cls) in m + n;; 40 CAP´ ITULO 3. L ´ OGICA PROPOSICIONAL Ahora podemos definir un algoritmo an´alogo al DP, pero reemplazando la regla de resoluci´on proposicional por la regla de divisi´on. let rec dpll clauses = if clauses = [] then true else if mem [] clauses then false else try dpll(one_literal_rule clauses) with Failure _ -> try dpll(affirmative_negative_rule clauses) with Failure _ -> let pvs = filter positive (unions clauses) in let p = maximize (posneg_count clauses) pvs in dpll (insert [p] clauses) or dpll (insert [negate p] clauses);; Como podemos ver en este algoritmo, la regla de divisi´on genera un ´arbol tal que si todas sus ramas contienen a , entonces el conjunto inicial de cl´ausulas es inconsistente; mientras que si alguna rama es el ∅, entonces el conjunto inicial de cl´ausulas es consistente. Una vez m´as, podemos aplicarlo a la verificaci´on de la satisfacibilidad o validez. let dpllsat fm = dpll(defcnfs fm);; let dplltaut fm = not(dpllsat(Not fm));; Y, como ejemplo: # dplltaut <<(p \/ (q /\ ˜r)) /\ s>>;; - : bool = false Cap´ıtulo 4 L´ogica de primer orden La l´ogica proposicional s´olo nos permite construir f´ormulas a partir de proposiciones primitivas que pueden ser independientemente verdaderas o falsas. Sin embargo, esto es demasiado restrictivo para captar los patrones de razonamiento donde la verdad o falsedad de las proposiciones dependen de los valores de las variables no proposicionales. La l´ogica de primer orden extiende la l´ogica proposicional con variables, predicados, funciones y cuantificadores. En este cap´ıtulo consideraremos la l´ogica de primer orden sin igualdad. 4.1. Sintaxis de la l´ogica de primer orden Un lenguaje de primer orden Σ es un conjunto de funciones, predicados y s´ımbolos de constantes, a partir de los cuales se construyen t´erminos y f´ormulas, pudiendo usar tambi´en para ello variables. Un lenguaje de primer orden est´a formado por: S´ımbolos l´ogicos: •las variables, denotadas por x, y, z, ...; •las conectivas l´ogicas heredadas de la l´ogica proposicional; •y los cuantificadores, de los que hablaremos posteriormente. S´ımbolos propios: •s´ımbolos de funci´on, denotados por f, g, ...; •s´ımbolos de predicado, P, Q, R, ...; •s´ımbolos de constantes. 41 48 CAP´ ITULO 4. L ´ OGICA DE PRIMER ORDEN F es satisfacible si tiene alguna realizaci´on. Si un conjunto de f´ormulas S tiene alguna realizaci´on se dice que es consistente. F es insatisfacible si no tiene ninguna realizaci´on. Si un conjunto de f´ormulas Sno tiene ninguna realizaci´on se dice que es inconsistente. Se puede probar la siguiente propiedad: una f´ormula Fes v´alida si y s´olo si ¬Fes insatisfacible. Al igual que en l´ogica proposicional, si F⇔Ges l´ogicamente v´alida decimos que FyGson l´ogicamente equivalentes. Se dice que Fes consecuencia l´ogica de S si todos los modelos de Slo son de F, y lo notamos S|=F. Usaremos la notaci´on S|=MFpara indicar que Mes un modelo espec´ıfico de Fsiempre que lo sea de S. Sea S={F1, ..., Fn}finito, donde las Fison f´ormulas cerradas. Entonces {F1, ..., Fn} |=Fes equivalente a F1∧... ∧Fn⇒F. No es posible implementar un algoritmo para decidir la validez o la satisfacibilidad de la l´ogica de primer orden directamente a trav´es de la sem´antica. No tenemos forma de verificar si una f´ormula de primer orden es satisfacible en una interpretaci´on con un dominio infinito. Sin embargo, se dar´a posteriormente un algoritmo para transformar f´ormulas manteniendo la equisatisfabilidad, y abordaremos el problema entonces. 4.3. Operaciones sint´acticas sobre f´ormulas Introduciremos algunas operaciones que usaremos posteriormente para la transformaci´on de f´ormulas en formas normales. Sea Funa f´ormula de primer orden y x1, ..., xnsus variables libres. Se denomina cierre universal de Fa∀x1, ..., xn.F. Se demuestra que una f´ormula es v´alida si y s´olo si su cierre universal lo es, y es m´as conveniente trabajar con f´ormulas cerradas. As´ı, como explicamos antes, si todas las f´ormulas que intervienen son cerradas tenemos: {F1, ..., Fn} |=F⇔F1∧... ∧Fn⇒F Fes v´alida ⇔ ¬Fes insatisfacible Implementamos en OCaml el concepto de cierre universal: let generalize fm = itlist mk_forall (fv fm) fm;; Se define tambi´en el concepto de cierre existencial de una f´ormula Fcomo ∃x1...xn.F, donde x1,...,xnson las variables libres de F. Se demuestra que una f´ormula es satisfacible si y s´olo si su cierre existencial lo es. 4.3. OPERACIONES SINT ´ ACTICAS SOBRE F ´ ORMULAS 49 Otra operaci´on que necesitamos definir es la sustituci´on de una variable por un t´ermino en otro t´ermino o una f´ormula. Por ejemplo, sustituir xpor 1 en x < 2⇒x≤ypara obtener 1 <2⇒1≤y. Una sustituci´on σde Σ es una aplicaci´on σ:V ar −→ Term(Σ). Denotaremos las sustituciones por [x1/t1, ..., xn/tn]. Especificaremos la sustituci´on como una funci´on sfn de los nombres de las variables en t´erminos. Para las variables que no queremos cambiar ´estos pueden ser indefinidos o simplemente la misma variable. let rec tsubst sfn tm = match tm with Var x -> tryapplyd sfn x tm | Fn(f,args) -> Fn(f,map (tsubst sfn) args);; Para aplicar la sustituci´on a f´ormulas debemos tener m´as cuidado, debido a las variables ligadas. Sin embargo, a´un evitando las sustituciones de dichas variables, corremos el riesgo de sustituir una variable libre por otra que en nuestra f´ormula est´e ligada. Por ejemplo, reemplazar ypor xen la f´ormula ∃x.x + 1 = yda como resultado ∃x.x + 1 = x, que no es lo que quer´ıamos, pues hemos obtenido una f´ormula cerrada. Para evitar esto, en primer lugar, vamos a renombrar las variables ligadas que sean necesarias. Implementamos una funci´on en Ocaml que a˜nada caracteres a la variable hasta que sea distinta de todas las variables de un lista dada. let rec variant x vars = if mem x vars then variant (xˆ"’") vars else x;; Por ejemplo: # variant "x" ["y"; "z"];; - : string = "x" # variant "x" ["x"; "y"];; - : string = "x’" # variant "x" ["x"; "x’"];; - : string = "x’’" Ahora, la definici´on de sustituci´on empieza con una serie de sencillas recursiones estructurales. Sin embargo, los dos casos m´as delicados de f´ormulas cuantificadas, ∀x.F y∃x.F son son tratados por otra funci´on mutuamente recursiva substq. 50 CAP´ ITULO 4. L ´ OGICA DE PRIMER ORDEN let rec subst subfn fm = match fm with False -> False | True -> True | Atom(R(p,args)) -> Atom(R(p,map (tsubst subfn) args)) | Not(p) -> Not(subst subfn p) | And(p,q) -> And(subst subfn p,subst subfn q) | Or(p,q) -> Or(subst subfn p,subst subfn q) | Imp(p,q) -> Imp(subst subfn p,subst subfn q) | Iff(p,q) -> Iff(subst subfn p,subst subfn q) | Forall(x,p) -> substq subfn mk_forall x p | Exists(x,p) -> substq subfn mk_exists x p and substq subfn quant x p = let x’ = if exists (fun y -> mem x (fvt(tryapplyd subfn y (Var y)))) (subtract (fv p) [x]) then variant x (fv(subst (undefine x subfn) p)) else x in quant x’ (subst ((x |-> Var x’) subfn) p);; Esta funci´on substq comprueba si existe alguna variable libre y6=xtal que aplicar la sustituci´on a ydevuelve un t´ermino con xlibre. Si es as´ı, toma una nueva variable x0que no entrar´a en conflicto con ninguna de las otras sustituciones en F. Entonces se aplica la sustituci´on a pcambiando xpor x0. Por ejemplo: # subst ("y" |=> Var "x") <<forall x. x = y>>;; - : fol formula = <<forall x’. x’ = x>> # subst ("y" |=> Var "x") <<forall x x’. x = y ==> x = x’>>;; - : fol formula = <<forall x’ x’’. x’ = x ==> x’ = x’’>> Obtenemos una propiedad importante: Si una f´ormula es v´alida cualquier sustituci´on de dicha f´ormula lo es. Una f´ormula Fse dice que est´a en forma rectificada si ninguna variable aparece libre y ligada simult´aneamente y cada cuantificador se refiere a una variable diferente. 4.4. Forma normal prenexa Una f´ormula de primer orden Fse dice que est´a en forma normal prenexa o PNF (del ingl´es, prenex normal form) si es de la forma (Q1x1)... (Qnxn)G, donde Qi∈ {∀,∃},n≥0 y Gno tiene cuantificadores. (Q1x1)... (Qnxn) se llama el prefijo de FyGse llama la matriz de F. Mostraremos en esta secci´on como transformar una f´ormula en otra l´ogicamente equivalente en forma normal prenexa. En primer lugar, debemos eliminar los cuantificadores vacuos en una f´ormula. Esto es, aquellos que cuantifican una variable ya cuantificada o una variable que 4.4. FORMA NORMAL PRENEXA 51 no aparece en la f´ormula. Para ello aplicaremos el siguiente resultado: si xno es una variable libre de F, tanto ∀x.F como ∃x.F son l´ogicamente equivalentes a F. Para definir la primera simplificaci´on de f´ormulas de primer orden, usando este resultado, haremos uso adem´as de la funci´on definida para l´ogica proposicional psimplify1: let simplify1 fm = match fm with Forall(x,p) -> if mem x (fv p) then fm else p | Exists(x,p) -> if mem x (fv p) then fm else p | _ -> psimplify1 fm;; Y podemos aplicarlo de manera recursiva a cada subf´ormula: let rec simplify fm = match fm with Not p -> simplify1 (Not(simplify p)) | And(p,q) -> simplify1 (And(simplify p,simplify q)) | Or(p,q) -> simplify1 (Or(simplify p,simplify q)) | Imp(p,q) -> simplify1 (Imp(simplify p,simplify q)) | Iff(p,q) -> simplify1 (Iff(simplify p,simplify q)) | Forall(x,p) -> simplify1(Forall(x,simplify p)) | Exists(x,p) -> simplify1(Exists(x,simplify p)) | _ -> fm;; Simplifiquemos como ejemplo la f´ormula (∀x y. P(x)∨(P(y)∧Falso)) ⇒ ∃z.Q: # simplify <<(forall x y. P(x) \/ (P(y) /\ false)) ==> exists z. Q>>;; - : fol formula = <<(forall x. P(x)) ==> Q>> A continuaci´on eliminamos los bicondicionales y las implicaciones e interiorizamos las negaciones. Para ello aplicamos las leyes de De Morgan que ya enunciamos cuando transform´abamos las f´ormulas proposicionales en formas normales negativas, y las leyes de De Morgan para cuantificadores, que enunciamos a continuaci´on: ¬(∀x.F)⇔ ∃x.¬F ¬(∃x.F)⇔ ∀x.¬F Lo implementamos en OCaml: 52 CAP´ ITULO 4. L ´ OGICA DE PRIMER ORDEN let rec nnf fm = match fm with And(p,q) -> And(nnf p,nnf q) | Or(p,q) -> Or(nnf p,nnf q) | Imp(p,q) -> Or(nnf(Not p),nnf q) | Iff(p,q) -> Or(And(nnf p,nnf q),And(nnf(Not p),nnf(Not q))) | Not(Not p) -> nnf p | Not(And(p,q)) -> Or(nnf(Not p),nnf(Not q)) | Not(Or(p,q)) -> And(nnf(Not p),nnf(Not q)) | Not(Imp(p,q)) -> And(nnf p,nnf(Not q)) | Not(Iff(p,q)) -> Or(And(nnf p,nnf(Not q)),And(nnf(Not p),nnf q)) | Forall(x,p) -> Forall(x,nnf p) | Exists(x,p) -> Exists(x,nnf p) | Not(Forall(x,p)) -> Exists(x,nnf(Not p)) | Not(Exists(x,p)) -> Forall(x,nnf(Not p)) | _ -> fm;; Por ejemplo: # nnf <<(forall x. P(x)) ==> ((exists y. Q(y)) <=> exists z. P(z) /\ Q(z))>>;; - : fol formula = <<(exists x. ˜P(x)) \/ (exists y. Q(y)) /\ (exists z. P(z) /\ Q(z)) \/ (forall y. ˜Q(y)) /\ (forall z. ˜P(z) \/ ˜Q(z))>> Tras estas transformaciones pasamos a la parte realmente distintiva de la forma normal prenexa: exteriorizar los cuantificadores. Para ello hacemos uso de las siguientes equivalencias, suponiendo que xno es libre en G: (∀x.F)∧G≡ ∀x. (F∧G) (∀x.F)∨G≡ ∀x. (F∨G) (∃x.F)∧G≡ ∃x. (F∧G) (∃x.F)∨G≡ ∃x. (F∨G) G∧(∀x.F)≡ ∀x. (G∧F) G∨(∀x.F)≡ ∀x. (G∨F) G∧(∃x.F)≡ ∃x. (G∨F) G∨(∃x.F)≡ ∃x. (G∨F) 4.4. FORMA NORMAL PRENEXA 53 Debemos tener cuidado al exteriorizar los cuantificadores con las variables libres. Por ejemplo: P(x)∧(∃x.Q(x)) no es l´ogicamente equivalente a ∃x. (P(x),∧Q(x)) pues la variable xes libre en la primera f´ormula pero no en la segunda. En estos casos, renombraremos la variable ligada, mediante la sustituci´on de ´esta por una variable que no aparezca en la f´ormula. Esto es, rectificaremos la f´ormula. En el ejemplo anterior la primera f´ormula s´ı ser´ıa l´ogicamente equivalente a ∃y. (P(x)∧Q(y)). Para exteriorizar los cuantificadores que ocurren como las subf´ormulas inmediatas de una conjunci´on o una disyunci´on, definimos la siguiente funci´on en Ocaml: let rec pullquants fm = match fm with And(Forall(x,p),Forall(y,q)) -> pullq(true,true) fm mk_forall mk_and x y p q | Or(Exists(x,p),Exists(y,q)) -> pullq(true,true) fm mk_exists mk_or x y p q | And(Forall(x,p),q) -> pullq(true,false) fm mk_forall mk_and x x p q | And(p,Forall(y,q)) -> pullq(false,true) fm mk_forall mk_and y y p q | Or(Forall(x,p),q) -> pullq(true,false) fm mk_forall mk_or x x p q | Or(p,Forall(y,q)) -> pullq(false,true) fm mk_forall mk_or y y p q | And(Exists(x,p),q) -> pullq(true,false) fm mk_exists mk_and x x p q | And(p,Exists(y,q)) -> pullq(false,true) fm mk_exists mk_and y y p q | Or(Exists(x,p),q) -> pullq(true,false) fm mk_exists mk_or x x p q | Or(p,Exists(y,q)) -> pullq(false,true) fm mk_exists mk_or y y p q | _ -> fm la cual llama a otra funci´on mutuamente recursiva a ´esta, para englobar varios casos similares: and pullq(l,r) fm quant op x y p q = let z = variant x (fv fm) in let p’ = if l then subst (x |=> Var z) p else p and q’ = if r then subst (y |=> Var z) q else q in quant z (pullquants(op p’ q’));; As´ı sustituir´ıamos las variables necesarias para exteriorizar los cuantificadores. Mediante lyrindicamos si hacemos la sustituci´on en la subf´ormula izquierda o derecha de la conectiva l´ogica, respectivamente. Mediante la funci´on variant se obtiene una variable que no haya aparecido a´un en la f´ormula, y hacemos la sustituci´on con dicha variable. Despu´es, vuelve a llamar a la funci´on pullquants. Aplicamos esto a la f´ormula completa de manera recursiva. 54 CAP´ ITULO 4. L ´ OGICA DE PRIMER ORDEN let rec prenex fm = match fm with Forall(x,p) -> Forall(x,prenex p) | Exists(x,p) -> Exists(x,prenex p) | And(p,q) -> pullquants(And(prenex p,prenex q)) | Or(p,q) -> pullquants(Or(prenex p,prenex q)) | _ -> fm;; Por ´ultimo, simplificando la f´ormula y haciendo uso de la forma normal negativa definida para f´ormulas de primer orden, implementamos la forma normal prenexa. let pnf fm = prenex(nnf(simplify fm));; Como ejemplo calculemos la forma normal prenexa de la f´ormula (∀x.(P(x)∨R(y))) ⇒ ∃y z.(Q(y)∨ ¬(∃z.(P(z)∧Q(z)))) En primer lugar simplifiquemos la f´ormula y calculemos su forma normal negativa: # nnf(simplify <<(forall x. P(x) \/ R(y)) ==> exists y z. Q(y) \/ ˜(exists z. P(z) /\ Q(z)) >>);; - : fol formula = <<(exists x. ˜P(x) /\ ˜R(y)) \/ (exists y. Q(y) \/ (forall z. ˜P(z) \/ ˜Q(z)))>> Podemos observar que en la f´ormula resultante, la variable ytiene tanto apariciones libres como ligadas. Por tanto debemos rectificarla. Para ello basta sustituir la variable ligada ypor x, ya que no entran en conflicto, y agrupar los dos cuantificadores existenciales en uno s´olo. As´ı, obtenemos: # pnf <<(forall x. P(x) \/ R(y)) ==> exists y z. Q(y) \/ ˜(exists z. P(z) /\ Q(z)) >>;; - : fol formula = <<exists x. forall z. ˜P(x) /\ ˜R(y) \/ Q(x) \/ ˜P(z) \/ ˜Q(z)>> 4.5. Forma de Skolem Una f´ormula Fse dice que est´a en forma normal de Skolem si es de la forma ∀x1...∀xn.G, donde n≥0 y G no tiene cuantificadores. Enunciamos a continuaci´on dos propiedades necesarias en el algoritmo para el c´alculo de la forma normal de Skolem: Si aes una constante que no ocurre en F, entonces ∃x.F ≈F[x/a]. ase denomina constante de Skolem. 4.5. FORMA DE SKOLEM 55 Si ges un s´ımbolo de funci´on n-aria que no ocurre en F, entonces: ∀x1...∀xn∃x.F ≈ ∀x1...∀xnF[x/g(x1, ..., xn)] gse denomina funci´on de Skolem. Aqu´ı F≈Gsimboliza FyGson equisatisfacibles. Recordamos la definici´on de equisatisfacibilidad: FyGson equisatisfacibles si Fes satisfacible si y s´olo si Ges satisfacible. Implementamos en Ocaml a continuaci´on un procedimiento para obtener las funciones que aparecen en una f´ormula de primer orden. Las identificaremos como pares nombre-aridad. let rec funcs tm = match tm with Var x -> [] | Fn(f,args) -> itlist (union ** funcs) args [f,length args];; let functions fm = atom_union (fun (R(p,a)) -> itlist (union ** funcs) a []) fm;; En el algoritmo que vamos a implementar para obtener la forma normal de Skolem de una f´ormula de primer orden Fno transformaremos previamente F en forma normal prenexa. Esto se debe a que el algoritmo para el c´alculo de la forma normal prenexa exterioriza los cuantificadores existenciales, introduciendo las variables libres de la f´ormula original en el alcance de dichos cuantificadores, por lo que las funciones de Skolem necesitar´ıan m´as argumentos. Por ejemplo, la forma normal de Skolem de la f´ormula ∀xz.(x=z∨ ∃y.(x·y= 1)) es ∀xz.(x=z∨x·f(x) = 1) mientras que si la transformamos primero en forma normal prenexa: ∀xz. ∃y.(x=z∨x·y= 1) su forma normal de Skolem es ∀xz.(x=z∨x·f(x, z) = 1) Sin embargo, para utilizar las funciones de Skolem necesitamos introducir las negaciones en la f´ormula original. Veamos un ejemplo: (∃y.P(y)) ∧ ¬(∃x.P(x)) 56 CAP´ ITULO 4. L ´ OGICA DE PRIMER ORDEN es insatisfacible mientras que si transformamos la subf´ormula derecha en forma normal de Skolem sin introducir previamente la negaci´on, la f´ormula resultante obtenida es satisfacible: (∃y.P(y)) ∧ ¬P(c) (4.1) Es por ello que, para mantener la satisfacibilidad o instisfacibilidad de la f´ormula original, en primer lugar transformaremos las f´ormulas en forma normal negativa. Para transformar una f´ormula en forma normal negativa descenderemos a trav´es de ella eliminando los cuantificadores existenciales mediante las funciones de Skolem y transformando las subf´ormulas en forma normal de Skolem. Evitaremos usar funciones de Skolem con el mismo nombre que las funciones que ya aparezcan en nuestra f´ormula, aunque tengan distinta aridad. let rec skolem fm fns = match fm with Exists(y,p) -> let xs = fv(fm) in let f = variant (if xs = [] then "c_"ˆy else "f_"ˆy) fns in let fx = Fn(f,map (fun x -> Var x) xs) in skolem (subst (y |=> fx) p) (f::fns) | Forall(x,p) -> let p’,fns’ = skolem p fns in Forall(x,p’),fns’ | And(p,q) -> skolem2 (fun (p,q) -> And(p,q)) (p,q) fns | Or(p,q) -> skolem2 (fun (p,q) -> Or(p,q)) (p,q) fns | _ -> fm,fns and skolem2 cons (p,q) fns = let p’,fns’ = skolem p fns in let q’,fns’’ = skolem q fns’ in cons(p’,q’),fns’’;; La funci´on skolem devuelve un par formado por la funci´on original en forma normal de Skolem y por las funciones que aparecen en el primer elemento del par. La funci´on skolem2 es una funci´on auxiliar para agrupar los casos de las conectivas binarias And yOr. La funci´on principal del algoritmo, que implementamos a continuaci´on, simplifica la f´ormula y la transforma en forma normal negativa. Despu´es aplica la funci´on skolem con un conjunto inicial apropiado de s´ımbolos de funciones a evitar. let askolemize fm = fst(skolem (nnf(simplify fm)) (map fst (functions fm)));; Implementamos las funciones siguientes para obtener la forma normal de Skolem de una f´ormula sin los cuantificadores universales, previamente exteriorizados, ni los existenciales, eliminados mediante la funci´on skolem: 4.6. TEOREMA DE HERBRAND 57 let rec specialize fm = match fm with Forall(x,p) -> specialize p | _ -> fm;; let skolemize fm = specialize(pnf(askolemize fm));; Veamos como ejemplo qu´e obtenemos al aplicar las funciones anteriores a la f´ormula ∃y.((x<y)⇒ ∀u∃v. x ∗u<y∗v): # askolemize <<exists y. x < y ==> forall u. exists v. x * u < y * v>>;; - : fol formula = <<˜x < f_y(x) \/ (forall u. x * u < f_y(x) * f_v(u,x))>> # skolemize <<exists y. x < y ==> forall u. exists v. x * u < y * v>>;; - : fol formula = <<˜x < f_y(x) \/ x * u < f_y(x) * f_v(u,x)>> # askolemize ( pnf <<exists y. x < y ==> forall u. exists v. x * u < y * v>>);; - : fol formula = <<forall u. ˜x < f_y(x) \/ x * u < f_y(x) * f_v(u,x)>> En el primer caso, obtenemos la forma normal de Skolem de una f´ormula sin transformarla previamente en forma normal prenexa y sin eliminar los cuantificadores al final. En el segundo caso hemos eliminado los cuantificadores de la f´ormula. En el ´ultimo caso hemos transformado la f´ormula previamente en forma normal prenexa y despu´es hemos aplicado el algoritmo para el c´alculo de la forma normal de Skolem. 4.6. Teorema de Herbrand Sea Lel lenguaje de primer orden sin igualdad. Definimos el universo de Herbrand de Lcomo el conjunto de los t´erminos b´asicos de L, esto es, todos los t´erminos que se pueden construir a partir de las constantes y los s´ımbolos de funci´on del lenguaje sin usar variables. Se representa por UH(L). Si el lenguaje no tiene constantes a˜nadimos una constante apara hacer el universo de Hebrand no vac´ıo. Sea Cel conjunto de constantes de LyFnel conjunto de s´ımbolos de funci´on n-aria de L. UH(L) = ∪i≥0Hi(L) donde Hi(L) es el nivel idel UH(L) definido por H0(L) = (C, si C6=∅ {a},en caso contrario Hi+1(L) = Hi(L)∪ {f(t1, ..., tn) : f∈Fnyt1, ..., tn∈Hi(L)} 64 CAP´ ITULO 5. ELIMINACI ´ ON DE CUANTIFICADORES Definamos una funci´on separate que transforme una f´ormula ∃x.(F1∧...∧Fn) en (∃x.(Fi∧... ∧Fj)) ∧(Fk∧... ∧Fl), donde los Fi,..., Fjson las f´ormulas con xlibre y Fk,..., Flson las dem´as. Las conjunciones de la f´ormula de entrada son presentadas como un conjunto cjs: let separate x cjs = let yes,no = partition (mem x ** fv) cjs in if yes = [] then list_conj no else if no = [] then Exists(x,list_conj yes) else And(Exists(x,list_conj yes),list_conj no);; Definimos ahora una funci´on pushquant, que dada una variable xy una f´ormula Ftransforma la f´ormula ∃x.F en una equivalente con el alcance del cuantificador existencial reducido. En primer lugar, si xno es libre en la f´ormula F, la respuesta es F. En otro caso, transformamos Fen forma normal disyuntiva, siendo de la forma ∃x.(C1∨... ∨Cn), donde cada Cies una conjunci´on de literales. Lo transformamos ahora en (∃x.C1)∨... ∨(∃x.Cn), y aplicamos a cada miembro de la disyunci´on la funci´on separate: let rec pushquant x p = if not (mem x (fv p)) then p else let djs = purednf(nnf p) in list_disj (map (separate x) djs);; Implementamos a continuaci´on una funci´on que transforma la f´ormula ∀x.G en ¬(∃x.¬G) y aplica pushquant posteriormente. Suponemos que la f´ormula inicial est´a en forma normal negativa, reduciendo as´ı los casos a tratar: let rec miniscope fm = match fm with Not p -> Not(miniscope p) | And(p,q) -> And(miniscope p,miniscope q) | Or(p,q) -> Or(miniscope p,miniscope q) | Forall(x,p) -> Not(pushquant x (Not(miniscope p))) | Exists(x,p) -> pushquant x (miniscope p) | _ -> fm;; 5.2. PROCEDIMIENTO DE ELIMINACI ´ ON DE CUANTIFICADORES 65 5.2.2. Funci´on principal Ahora definimos la funci´on principal. Notemos que es de orden superior, esto es, toma como argumentos varias funciones y devuelve otra funci´on. Sus argumentos son: afn: es una funci´on propia de cada teor´ıa, que se aplica a una lista de variables y a una f´ormula. Supongamos por el momento que afn vars fm simplemente devuelve su segundo argumento fm sin cambios. nfn: es una funci´on que transforma una f´ormula en forma normal disyuntiva. qfn: es la funci´on bfn que aparece en la anterior qelim. Es espec´ıfica de cada teor´ıa y elimina los cuantificadores de las f´ormulas de la forma ∃x.(α0(x)∧... ∧αn(x)) donde los αison literales. Cabe destacar que aunque estemos definiendo un procedimiento general de eliminaci´on de cuantificadores, como las funciones anteriores son propias de cada teor´ıa, ´esta admitir´a eliminaci´on de cuantificadores si podemos definir dichas funciones para la teor´ıa. Veamos c´omo act´ua la siguiente funci´on lift qelim sobre una f´ormula fm: 1. Simplificamos la f´ormula con la funci´on miniscope para aplicar el algoritmo a la subf´ormula m´as peque˜na posible. 2. Distingamos varios casos seg´un el tipo de f´ormula: a) Para las conectivas l´ogicas se lleva a cabo recursivamente el mismo procedimiento: la funci´on auxiliar qelift es aplicada a cada subf´ormula. b) Si la f´ormula est´a universalmente cuantificada, transformamos el cuantificador universal en existencial usando las Leyes de De Morgan. c) El caso m´as interesante entonces es el de una f´ormula existencialmente cuantificada: ∃x.p. 1) Se aplica de manera recursiva el procedimiento de eliminaci´on de cuantificadores a p, con lo que obtenemos una f´ormula sin cuantificadores equivalente a p. Denomin´emosla p0. 2) Obtenemos la forma normal disyuntiva de p0haciendo uso de nnf. Definimos djs como el conjunto de todas estas conjunciones. 3) Aplicamos la funci´on qelim a cada elemento de djs, tomando el argumento qfn como bfn, usando impl´ıcitamente la equivalencia: (∃x.(D1(x)∨... ∨Dn(x)) ⇔(∃x.D1(x)) ∨... ∨(∃x.Dn(x)). 66 CAP´ ITULO 5. ELIMINACI ´ ON DE CUANTIFICADORES Devuelve la disyunci´on de los elementos del conjunto anterior. 3. Por ´ultimo simplificamos la f´ormula resultante. let lift_qelim afn nfn qfn = let rec qelift vars fm = match fm with | Atom(R(_,_)) -> afn vars fm | Not(p) -> Not(qelift vars p) | And(p,q) -> And(qelift vars p,qelift vars q) | Or(p,q) -> Or(qelift vars p,qelift vars q) | Imp(p,q) -> Imp(qelift vars p,qelift vars q) | Iff(p,q) -> Iff(qelift vars p,qelift vars q) | Forall(x,p) -> Not(qelift vars (Exists(x,Not p))) | Exists(x,p) -> let djs = disjuncts(nfn(qelift (x::vars) p)) in list_disj(map (qelim (qfn vars) x) djs) | _ -> fm in fun fm -> simplify(qelift (fv fm) (miniscope fm));; La funci´on nnf es una versi´on mejorada de la transformaci´on a forma normal disyuntiva. Para ello construiremos a continuaci´on una versi´on mejorada de la forma normal negativa de una f´ormula. En primer lugar, nos gustar´ıa tener una funci´on para modificar literales, por ejemplo para transformar desigualdades negadas como ¬(s < t) en t≤s. A esta funci´on la denominaremos lfn. Esta funci´on ser´a propia de la teor´ıa en que trabajemos. En segundo lugar, a veces se realizar´an divisiones en casos seg´un una propiedad pde las otras variables, obteniendo una f´ormula de la forma (p∧q0)∨(¬p∧q1). En lugar de negarla y transformarla en forma normal disyuntiva, es menos costoso computacionalmente usar el hecho de que ¬((p∧q0)∨(¬p∧q1)) ⇔(p∧ ¬q0)∨(¬p∧ ¬q1) Veamos esta equivalencia: ¬((p∧q0)∨(¬p∧q1)) ⇔(¬p∨ ¬q0)∧(p∨ ¬q1)⇔ ⇔(¬p∧p)∨(¬p∧ ¬q1)∨(¬q0∧p)∨(¬q0∧ ¬q1) Como ¬p∧pes una contradicci´on, obtenemos (¬p∧p)∨(¬p∧¬q1)∨(¬q0∧p)∨(¬q0∧¬q1)⇔(¬p∧¬q1)∨(¬q0∧p)∨(¬q0∧¬q1) Adem´as, bien po bien ¬pdebe ser ’Verdadero’: 5.3. TEOR´ IA DE LOS ´ ORDENES LINEALES DENSOS 67 p’Verdadero y (¬q0∧p) ’Falso’ ⇒ ¬q0’Falso’ ⇒(¬q0∧ ¬q1) ’Falso’. p’Falso’ y (¬p∧ ¬q1) ’Falso’ ⇒ ¬q1’Falso’ ⇒(¬q0∧ ¬q1) es ’Falso’. Rec´ıprocamente, si (¬q0∧ ¬q1) es ’Falso’, entonces (¬p∧ ¬q1)∨(¬q0∧p)∨(¬q0∧ ¬q1)⇔(¬p∧ ¬q1)∨(¬q0∧p) Tenemos por tanto la equivalencia. Usando todo esto definiremos la funci´on cnnf, simplificando la f´ormula tanto al principio como al final: let cnnf lfn = let rec cnnf fm = match fm with And(p,q) -> And(cnnf p,cnnf q) | Or(p,q) -> Or(cnnf p,cnnf q) | Imp(p,q) -> Or(cnnf(Not p),cnnf q) | Iff(p,q) -> Or(And(cnnf p,cnnf q),And(cnnf(Not p),cnnf(Not q))) | Not(Not p) -> cnnf p | Not(And(p,q)) -> Or(cnnf(Not p),cnnf(Not q)) | Not(Or(And(p,q),And(p’,r))) when p’ = negate p -> Or(cnnf (And(p,Not q)),cnnf (And(p’,Not r))) | Not(Or(p,q)) -> And(cnnf(Not p),cnnf(Not q)) | Not(Imp(p,q)) -> And(cnnf p,cnnf(Not q)) | Not(Iff(p,q)) -> Or(And(cnnf p,cnnf(Not q)), And(cnnf(Not p),cnnf q)) | _ -> lfn fm in simplify ** cnnf ** simplify;; 5.3. Teor´ıa de los ´ordenes lineales densos La teor´ıa de los ´ordenes lineales densos sin extremos (DLO, del ingl´es ’dense linear orders’) est´a basada en un lenguaje conteniendo el predicado binario ’<’ y la igualdad sin s´ımbolos de funci´on. Puede ser axiomatizada por el siguiente conjunto finito de f´ormulas cerradas: ∀x y. x =y∨x<y∨y < x, ∀x y z. x < y ∧y < z ⇒x < z, ∀x. ¬(x<x), ∀x y. x < y ⇒ ∃z.x < z ∧z < y, ∀x.∃y. x < y, ∀x.∃y. y < x. Las tres primeras expresan que ’<’ es un orden lineal. La siguiente asegura la densidad, esto es, que entre cada par de elementos hay otro. Las dos ´ultimas f´ormulas afirman que no hay extremos. 68 CAP´ ITULO 5. ELIMINACI ´ ON DE CUANTIFICADORES 5.3.1. Igualdad En lo que sigue usaremos la igualdad como un predicado binario, y es por ello que necesitamos implementarla en Ocaml. En muchas aplicaciones de la l´ogica, las ecuaciones juegan un papel central. Podemos definir operaciones sint´acticas para probar si una f´ormula es una ecuaci´on o para obtener los dos t´erminos que forman una ecuaci´on: let is_eq = function (Atom(R("=",_))) -> true | _ -> false;; let dest_eq fm = match fm with Atom(R("=",[s;t])) -> s,t | _ -> failwith "dest_eq: not an equation";; 5.3.2. Eliminaci´on de cuantificadores para DLO Esta teor´ıa admite eliminaci´on de cuantificadores, como mostr´o Langford [7], y daremos un algoritmo expl´ıcito para ella. Por los resultados ya vistos, basta considerar una f´ormula ∃x.(l1(x)∧... ∧ln(x)), donde cada li(x) es un literal que contiene a x. Para implementar el procedimiento usaremos la funci´on lift qelim. Para ello debemos definir: afn, que denominaremos afn dlo. nfn como dnf ** cnnf lfn dlo, donde s´olo nos queda definir lfn dlo, que es el argumento lfn de la funci´on ya definida cnnf. qfn, que denominaremos dlobasic, y ser´a el n´ucleo del procedimiento. Definimos en primer lugar la funci´on afn dlo como una transformaci´on inicial para permitirnos usar otras relaciones de desigualdad: s≤t⇔ ¬(t<s), s≥t⇔ ¬(s<t), s>t⇔t<s. let afn_dlo vars fm = match fm with Atom(R("<=",[s;t])) -> Not(Atom(R("<",[t;s]))) | Atom(R(">=",[s;t])) -> Not(Atom(R("<",[s;t]))) | Atom(R(">",[s;t])) -> Atom(R("<",[t;s])) | _ -> fm;; 5.3. TEOR´ IA DE LOS ´ ORDENES LINEALES DENSOS 69 A continuaci´on definiremos la funci´on lfn dlo como una modificaci´on de literales espec´ıfica para esta teor´ıa, bas´andonos en las equivalencias: ¬(s<t)⇔s=t∨t < s ¬(s=t)⇔s<t∨t < s let lfn_dlo fm = match fm with Not(Atom(R("<",[s;t]))) -> Or(Atom(R("=",[s;t])),Atom(R("<",[t;s]))) | Not(Atom(R("=",[s;t]))) -> Or(Atom(R("<",[s;t])),Atom(R("<",[t;s]))) | _ -> fm;; Nos centraremos por ´ultimo en la funci´on dlobasic, que es el n´ucleo del procedimiento. Esta funci´on toma como argumento una f´ormula de la forma ∃x.F, donde Fes una conjunci´on de literales, y devuelve una f´ormula equivalente a la anterior sin cuantificadores. Ya que no hay s´ımbolos de funci´on en esta teor´ıa podemos suponer que todos los literales de Fson ´atomos. Deben ser de la forma x < y ox=ypara ciertas variables xey. Cualquier ´atomo de la forma x=xes trivialmente verdadero y puede ser ignorado; los dem´as se recogen en una lista cjs. Si algunos de estos es una ecuaci´on, entonces, como todos los literales contienen a la variable cuantificada, debe ser de la forma x=yoy=x, donde xes la variable existencialmente cuantificada que queremos eliminar e yes otra variable. En este caso podemos obtener una f´ormula l´ogicamente equivalente eliminando el cuantificador y sustituyendo xen las otras subf´ormulas; esto s´olo refleja las equivalencias l´ogicas como (∃x. x =y∧P(x, y)) ⇔P(y, y) Si este paso no puede ser aplicado, entonces todos los ´atomos deben ser inecuaciones. Si alguno es de la forma x<x, entonces ´el y la f´ormula son trivialmente falsos. En otro caso definimos ls como el conjunto de los t´erminos sique aparecen en inecuaciones si< x, y como rs el conjunto de los t´erminos que aparecen en inecuaciones x < tj. Notemos ahora que en esta teor´ıa: T(∃x.(^ i si< x)∧(^ j x<tj)) ⇔(^ i,j si< tj) Justifiquemos este paso. Si si< x ∧x<tj, usando el axioma de transitividad, concluimos que si< tj. Rec´ıprocamente, si Vi,j si< tj, tomando el mayor de los siy el menor de los tjy aplicando el axioma de densidad obtenemos que ^ i,j (si< x ∧x<tj) Concluimos el resultado gracias al axioma de transitividad. 70 CAP´ ITULO 5. ELIMINACI ´ ON DE CUANTIFICADORES Si no hay desigualdades de alguno de los dos tipos (ls ors son vac´ıos), la f´ormula es equivalente a ’Verdadero’, ya que los axiomas de la teor´ıa afirman que no hay extremos. Como list conj devuelve >para la lista vac´ıa, estos casos ya estar´ıan resueltos en la implementaci´on: let dlobasic fm = match fm with Exists(x,p) -> let cjs = subtract (conjuncts p) [Atom(R("=",[Var x;Var x]))] in try let eqn = find is_eq cjs in let s,t = dest_eq eqn in let y = if s = Var x then t else s in list_conj(map (subst (x |=> y)) (subtract cjs [eqn])) with Failure _ -> if mem (Atom(R("<",[Var x;Var x]))) cjs then False else let lefts,rights = partition (fun (Atom(R("<",[s;t]))) -> t = Var x) cjs in let ls = map (fun (Atom(R("<",[l;_]))) -> l) lefts and rs = map (fun (Atom(R("<",[_;r]))) -> r) rights in list_conj(allpairs (fun l r -> Atom(R("<",[l;r]))) ls rs) | _ -> failwith "dlobasic";; Finalmente usamos la funci´on lift qelim para definir el procedimiento, como ya anticip´abamos: let quelim_dlo = lift_qelim afn_dlo (dnf ** cnnf lfn_dlo) (fun v -> dlobasic);; 5.3.3. Ejemplos Veamos en primer lugar un ejemplo sencillo: ∃z.(z < x ∧z < y) Esta f´ormula es del tipo ∃z.F, donde Fes una conjunci´on de literales, por lo que no hay que aplicarle transformaciones previas. Dichos literales son inecuaciones, ambos de la forma z < tj. Entonces esta f´ormula es trivialmente verdadera, ya que los axiomas de la teor´ıa afirman que no hay extremos (∀x. ∃y. y < x): # quelim_dlo <<exists z. z < x /\ z < y>>;; - : fol formula = <<true>> La f´ormula ∃z.(x<z∧z < y) 5.3. TEOR´ IA DE LOS ´ ORDENES LINEALES DENSOS 71 tambi´en es del tipo ∃z.F, con Fes una conjunci´on de literales. Adem´as dichos literales son tambi´en inecuaciones. Por el axioma de transitividad, como x < z y z < y tenemos que: ∃z.(x < z ∧z < y)⇔x < y, la cual es una f´ormula sin cuantificadores. # quelim_dlo <<exists z. x < z /\ z < y>>;; - : fol formula = <<x < y>> Veamos otro ejemplo. La f´ormula ∀x.(x<a⇒x<b) es un ejemplo de una f´ormula a la que hay que realizarle transformaciones previas. Aplicando las Leyes de De Morgan: ∀x.(x<a⇒x<b)⇔ ¬∃x.¬(x<a⇒x<b) Por tanto, la f´ormula a la que debemos aplicar el procedimiento es ∃x.¬(x<a⇒x<b) Transformando el cuerpo en forma normal negativa: ∃x.¬(x<a⇒x<b)⇔ ∃x.(x<a∧ ¬(x<b)) Podemos aplicar adem´as una desigualdad propia de esta teor´ıa: ¬(x<b)⇔x=b∨b < x Entonces: ∃x.¬(x<a⇒x<b)⇔ ∃x.((x<a∧x=b)∨(x < a ∧b<x)) ⇔ ⇔ ∃x.(x<a∧x=b)∨ ∃x.(x<a∧b<x) Aplicamos por tanto el procedimiento de eliminaci´on de cuantificadores a ambas subf´ormulas existencialmente cuantificadas. En el primer caso, como uno de los literales es la ecuaci´on x=b, eliminamos el cuantificador sustituyendo xpor b en los dem´as literales. El segundo caso es similar al ejemplo anterior. ∃x.(x<a∧x=b)⇔b<a ∃x.(x<a∧b<x)⇔b < a Finalmente hemos conseguido eliminar el cuantificador universal: ∀x.(x < a ⇒x<b)⇔ ¬(b<a∨b < a)⇔ ¬(b<a) 72 CAP´ ITULO 5. ELIMINACI ´ ON DE CUANTIFICADORES # quelim_dlo <<(forall x. x < a ==> x < b)>>;; - : fol formula = <<˜(b < a \/ b < a)>> Entonces, si aplicamos el procedimiento de eliminaci´on de cuantificadores a la f´ormula ∀a b. ((∀x.x < a ⇒x<b)⇔a≤b) debemos obtener que es una tautolog´ıa, debido al ejemplo anterior. # quelim_dlo <<forall a b. (forall x. x < a ==> x < b) <=> a <= b>>;; - : fol formula = <<true>> Bibliograf´ıa [1] Instalaci´on de ocaml. https://ocaml.org/docs/install.html. Accedido por ´ultima vez el 13-06-2016. [2] Ocaml. https://ocaml.org/. Accedido por ´ultima vez el 13-06-2016. [3] Aaron R Bradley and Zohar Manna. The calculus of computation: decision procedures with applications to verification. Springer Science & Business Media, 2007. [4] Amine Chaieb and Tobias Nipkow. Verifying and reflecting quantifier elimination for presburger arithmetic. [5] Herbert B Enderton. A mathematical introduction to logic. Academic press, 2001. [6] John Harrison. Handbook of practical logic and automated reasoning. Cambridge University Press, 2009. [7] Cooper Harold Langford. Some theorems on deducibility. Annals of Mathematics, pages 16–40, 1926. [8] Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier R´emy, and J´erˆome Vouillon. The ocaml system: Documentation and user’s manual. INRIA, release, 4. [9] Shashi Mohan Srivastava. A course on mathematical logic. Springer Science & Business Media, 2013. 73 80 AP´ ENDICE A. C ´ ODIGO (* ------------------------------------------------------------------------- *) let rec mem x lis = match lis with [] -> false | (h::t) -> Pervasives.compare x h = 0 || mem x t;; (* ------------------------------------------------------------------------- *) (* Explosi´ on de cadenas. *) (* ------------------------------------------------------------------------- *) let explode s = let rec exap n l = if n < 0 then l else exap (n - 1) ((String.sub s n 1)::l) in exap (String.length s - 1) [];; (* ------------------------------------------------------------------------- *) (* ´ Arboles. *) (* ------------------------------------------------------------------------- *) type (’a,’b)func = Empty | Leaf of int * (’a*’b)list | Branch of int * int * (’a,’b)func * (’a,’b)func;; (* ------------------------------------------------------------------------- *) (* Funci´ on indefinida. *) (* ------------------------------------------------------------------------- *) let undefined = Empty;; (* ------------------------------------------------------------------------- *) (* Operaciones fold para ´ arboles. *) (* ------------------------------------------------------------------------- *) let foldl = let rec foldl_list f a l = match l with [] -> a | (x,y)::t -> foldl_list f (f a x y) t in let rec foldl f a t = match t with Empty -> a | Leaf(h,l) -> foldl_list f a l | Branch(p,b,l,r) -> foldl f (foldl f a l) r in 81 foldl;; (* ------------------------------------------------------------------------- *) (* Grafo de una funci´ on. *) (* ------------------------------------------------------------------------- *) let graph f = setify (foldl (fun a x y -> (x,y)::a) [] f);; (* ------------------------------------------------------------------------- *) (* Aplicaci´ on. *) (* ------------------------------------------------------------------------- *) let applyd = let rec apply_listd l d x = match l with (a,b)::t -> let c = Pervasives.compare x a in if c = 0 then b else if c > 0 then apply_listd t d x else d x |[]->dxin fun f d x -> let k = Hashtbl.hash x in let rec look t = match t with Leaf(h,l) when h = k -> apply_listd l d x | Branch(p,b,l,r) when (k lxor p) land (b - 1) = 0 -> look (if k land b = 0 then l else r) |_->dxin look f;; let apply f = applyd f (fun x -> failwith "apply");; let tryapplyd f a d = applyd f (fun x -> d) a;; (* ------------------------------------------------------------------------- *) (* Indefinido. *) (* ------------------------------------------------------------------------- *) let undefine = let rec undefine_list x l = match l with (a,b as ab)::t -> let c = Pervasives.compare x a in if c = 0 then t else if c < 0 then l else let t’ = undefine_list x t in if t’ == t then l else ab::t’ | [] -> [] in 82 AP´ ENDICE A. C ´ ODIGO fun x -> let k = Hashtbl.hash x in let rec und t = match t with Leaf(h,l) when h = k -> let l’ = undefine_list x l in if l’ == l then t else if l’ = [] then Empty else Leaf(h,l’) | Branch(p,b,l,r) when k land (b - 1) = p -> if k land b = 0 then let l’ = und l in if l’ == l then t else (match l’ with Empty -> r | _ -> Branch(p,b,l’,r)) else let r’ = und r in if r’ == r then t else (match r’ with Empty -> l | _ -> Branch(p,b,l,r’)) |_->tin und;; (* ------------------------------------------------------------------------- *) (* Redfinici´ on y combinaci´ on. *) (* ------------------------------------------------------------------------- *) let (|->),combine = let newbranch p1 t1 p2 t2 = let zp = p1 lxor p2 in let b = zp land (-zp) in let p = p1 land (b - 1) in if p1 land b = 0 then Branch(p,b,t1,t2) else Branch(p,b,t2,t1) in let rec define_list (x,y as xy) l = match l with (a,b as ab)::t -> let c = Pervasives.compare x a in if c = 0 then xy::t else if c < 0 then xy::l else ab::(define_list xy t) | [] -> [xy] and combine_list op z l1 l2 = match (l1,l2) with [],_ -> l2 | _,[] -> l1 | ((x1,y1 as xy1)::t1,(x2,y2 as xy2)::t2) -> let c = Pervasives.compare x1 x2 in 83 if c < 0 then xy1::(combine_list op z t1 l2) else if c > 0 then xy2::(combine_list op z l1 t2) else let y = op y1 y2 and l = combine_list op z t1 t2 in if z(y) then l else (x1,y)::l in let (|->) x y = let k = Hashtbl.hash x in let rec upd t = match t with Empty -> Leaf (k,[x,y]) | Leaf(h,l) -> if h = k then Leaf(h,define_list (x,y) l) else newbranch h t k (Leaf(k,[x,y])) | Branch(p,b,l,r) -> if k land (b - 1) <> p then newbranch p t k (Leaf(k,[x,y])) else if k land b = 0 then Branch(p,b,upd l,r) else Branch(p,b,l,upd r) in upd in let rec combine op z t1 t2 = match (t1,t2) with Empty,_ -> t2 | _,Empty -> t1 | Leaf(h1,l1),Leaf(h2,l2) -> if h1 = h2 then let l = combine_list op z l1 l2 in if l = [] then Empty else Leaf(h1,l) else newbranch h1 t1 h2 t2 | (Leaf(k,lis) as lf),(Branch(p,b,l,r) as br) -> if k land (b - 1) = p then if k land b = 0 then (match combine op z lf l with Empty -> r | l’ -> Branch(p,b,l’,r)) else (match combine op z lf r with Empty -> l | r’ -> Branch(p,b,l,r’)) else newbranch k lf p br | (Branch(p,b,l,r) as br),(Leaf(k,lis) as lf) -> if k land (b - 1) = p then if k land b = 0 then (match combine op z l lf with Empty -> r | l’ -> Branch(p,b,l’,r)) else (match combine op z r lf with Empty -> l | r’ -> Branch(p,b,l,r’)) else newbranch p br k lf 84 AP´ ENDICE A. C ´ ODIGO | Branch(p1,b1,l1,r1),Branch(p2,b2,l2,r2) -> if b1 < b2 then if p2 land (b1 - 1) <> p1 then newbranch p1 t1 p2 t2 else if p2 land b1 = 0 then (match combine op z l1 t2 with Empty -> r1 | l -> Branch(p1,b1,l,r1)) else (match combine op z r1 t2 with Empty -> l1 | r -> Branch(p1,b1,l1,r)) else if b2 < b1 then if p1 land (b2 - 1) <> p2 then newbranch p1 t1 p2 t2 else if p1 land b2 = 0 then (match combine op z t1 l2 with Empty -> r2 | l -> Branch(p2,b2,l,r2)) else (match combine op z t1 r2 with Empty -> l2 | r -> Branch(p2,b2,l2,r)) else if p1 = p2 then (match (combine op z l1 l2,combine op z r1 r2) with (Empty,r) -> r | (l,Empty) -> l | (l,r) -> Branch(p1,b1,l,r)) else newbranch p1 t1 p2 t2 in (|->),combine;; let (|=>) = fun x y -> (x |-> y) undefined;; (* ------------------------------------------------------------------------- *) (* An´ alisis l´ exico. *) (* ------------------------------------------------------------------------- *) let matches s = let chars = explode s in fun c -> mem c chars;; let space = matches " \t\n\r" and punctuation = matches "()[]{}," and symbolic = matches "˜‘!@#$%ˆ&*-+=|\\:;<>.?/" and numeric = matches "0123456789" and alphanumeric = matches "abcdefghijklmnopqrstuvwxyz_’ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789";; let rec lexwhile prop inp = match inp with c::cs when prop c -> let tok,rest = lexwhile prop cs in cˆtok,rest | _ -> "",inp;; let rec lex inp = match snd(lexwhile space inp) with 85 [] -> [] | c::cs -> let prop = if alphanumeric(c) then alphanumeric else if symbolic(c) then symbolic else fun c -> false in let toktl,rest = lexwhile prop cs in (cˆtoktl)::lex rest;; (* ------------------------------------------------------------------------- *) (* Parser. *) (* ------------------------------------------------------------------------- *) let make_parser pfn s = let expr,rest = pfn (lex(explode s)) in if rest = [] then expr else failwith "Unparsed input";; (* ========================================================================= *) (* Sintaxis de la l´ ogica proposicional. *) (* ========================================================================= *) type (’a)formula = False | True | Atom of ’a | Not of (’a)formula | And of (’a)formula * (’a)formula | Or of (’a)formula * (’a)formula | Imp of (’a)formula * (’a)formula | Iff of (’a)formula * (’a)formula | Forall of string * (’a)formula | Exists of string * (’a)formula;; (* ------------------------------------------------------------------------- *) (* Parsing general. *) (* ------------------------------------------------------------------------- *) let rec parse_ginfix opsym opupdate sof subparser inp = let e1,inp1 = subparser inp in if inp1 <> [] && hd inp1 = opsym then parse_ginfix opsym opupdate (opupdate sof e1) subparser (tl inp1) else sof e1,inp1;; let parse_left_infix opsym opcon = parse_ginfix opsym (fun f e1 e2 -> opcon(f e1,e2)) (fun x -> x);; let parse_right_infix opsym opcon = parse_ginfix opsym (fun f e1 e2 -> f(opcon(e1,e2))) (fun x -> x);; 86 AP´ ENDICE A. C ´ ODIGO let parse_list opsym = parse_ginfix opsym (fun f e1 e2 -> (f e1)@[e2]) (fun x -> [x]);; let papply f (ast,rest) = (f ast,rest);; let nextin inp tok = inp <> [] && hd inp = tok;; let parse_bracketed subparser cbra inp = let ast,rest = subparser inp in if nextin rest cbra then ast,tl rest else failwith "Closing bracket expected";; (* ------------------------------------------------------------------------- *) (* Parsing de f´ ormulas. *) (* ------------------------------------------------------------------------- *) let rec parse_atomic_formula (ifn,afn) vs inp = match inp with [] -> failwith "formula expected" | "false"::rest -> False,rest | "true"::rest -> True,rest | "("::rest -> (try ifn vs inp with Failure _ -> parse_bracketed (parse_formula (ifn,afn) vs) ")" rest) | "˜"::rest -> papply (fun p -> Not p) (parse_atomic_formula (ifn,afn) vs rest) | "forall"::x::rest -> parse_quant (ifn,afn) (x::vs) (fun (x,p) -> Forall(x,p)) x rest | "exists"::x::rest -> parse_quant (ifn,afn) (x::vs) (fun (x,p) -> Exists(x,p)) x rest | _ -> afn vs inp and parse_quant (ifn,afn) vs qcon x inp = match inp with [] -> failwith "Body of quantified term expected" | y::rest -> papply (fun fm -> qcon(x,fm)) (if y = "." then parse_formula (ifn,afn) vs rest else parse_quant (ifn,afn) (y::vs) qcon y rest) and parse_formula (ifn,afn) vs inp = parse_right_infix "<=>" (fun (p,q) -> Iff(p,q)) (parse_right_infix "==>" (fun (p,q) -> Imp(p,q)) (parse_right_infix "\\/" (fun (p,q) -> Or(p,q)) (parse_right_infix "/\\" (fun (p,q) -> And(p,q)) 87 (parse_atomic_formula (ifn,afn) vs)))) inp;; (* ------------------------------------------------------------------------- *) (* Printing de f´ ormulas. *) (* ------------------------------------------------------------------------- *) let bracket p n f x y = (if p then print_string "(" else ()); open_box n; f x y; close_box(); (if p then print_string ")" else ());; let rec strip_quant fm = match fm with Forall(x,(Forall(y,p) as yp)) | Exists(x,(Exists(y,p) as yp)) -> let xs,q = strip_quant yp in x::xs,q | Forall(x,p) | Exists(x,p) -> [x],p | _ -> [],fm;; let print_formula pfn = let rec print_formula pr fm = match fm with False -> print_string "false" | True -> print_string "true" | Atom(pargs) -> pfn pr pargs | Not(p) -> bracket (pr > 10) 1 (print_prefix 10) "˜" p | And(p,q) -> bracket (pr > 8) 0 (print_infix 8 "/\\") p q | Or(p,q) -> bracket (pr > 6) 0 (print_infix 6 "\\/") p q | Imp(p,q) -> bracket (pr > 4) 0 (print_infix 4 "==>") p q | Iff(p,q) -> bracket (pr > 2) 0 (print_infix 2 "<=>") p q | Forall(x,p) -> bracket (pr > 0) 2 print_qnt "forall" (strip_quant fm) | Exists(x,p) -> bracket (pr > 0) 2 print_qnt "exists" (strip_quant fm) and print_qnt qname (bvs,bod) = print_string qname; do_list (fun v -> print_string " "; print_string v) bvs; print_string "."; print_space(); open_box 0; print_formula 0 bod; close_box() and print_prefix newpr sym p = print_string sym; print_formula (newpr+1) p and print_infix newpr sym p q = print_formula (newpr+1) p; print_string(" "ˆsym); print_space(); print_formula newpr q in print_formula 0;; let print_qformula pfn fm = 88 AP´ ENDICE A. C ´ ODIGO open_box 0; print_string "<<"; open_box 0; print_formula pfn fm; close_box(); print_string ">>"; close_box();; (* ------------------------------------------------------------------------- *) (* Variables proposicionales. *) (* ------------------------------------------------------------------------- *) type prop = P of string;; let pname(P s) = s;; (* ------------------------------------------------------------------------- *) (* Parsing y printing de f´ ormulas proposicionales. *) (* ------------------------------------------------------------------------- *) let parse_propvar vs inp = match inp with p::oinp when p <> "(" -> Atom(P(p)),oinp | _ -> failwith "parse_propvar";; let parse_prop_formula = make_parser (parse_formula ((fun _ _ -> failwith ""),parse_propvar) []);; let default_parser = parse_prop_formula;; let print_propvar prec p = print_string(pname p);; let print_prop_formula = print_qformula print_propvar;; #install_printer print_prop_formula;; (* ------------------------------------------------------------------------- *) (* Ejemplo. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; let fm = <<p ==> q <=> r /\ s \/ (t <=> ˜ ˜u /\ v)>>;; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Constructores como funciones. *) (* ------------------------------------------------------------------------- *) let mk_and p q = And(p,q) and mk_or p q = Or(p,q) and mk_imp p q = Imp(p,q) and mk_iff p q = Iff(p,q) 89 and mk_forall x p = Forall(x,p) and mk_exists x p = Exists(x,p);; (* ------------------------------------------------------------------------- *) (* Destructores. *) (* ------------------------------------------------------------------------- *) let dest_iff fm = match fm with Iff(p,q) -> (p,q) | _ -> failwith "dest_iff";; let dest_and fm = match fm with And(p,q) -> (p,q) | _ -> failwith "dest_and";; let rec conjuncts fm = match fm with And(p,q) -> conjuncts p @ conjuncts q | _ -> [fm];; let dest_or fm = match fm with Or(p,q) -> (p,q) | _ -> failwith "dest_or";; let rec disjuncts fm = match fm with Or(p,q) -> disjuncts p @ disjuncts q | _ -> [fm];; let dest_imp fm = match fm with Imp(p,q) -> (p,q) | _ -> failwith "dest_imp";; let antecedent fm = fst(dest_imp fm);; let consequent fm = snd(dest_imp fm);; (* ------------------------------------------------------------------------- *) (* Aplicar una funci´ on a los ´ atomos. *) (* ------------------------------------------------------------------------- *) let rec onatoms f fm = match fm with Atom a -> f a | Not(p) -> Not(onatoms f p) | And(p,q) -> And(onatoms f p,onatoms f q) | Or(p,q) -> Or(onatoms f p,onatoms f q) | Imp(p,q) -> Imp(onatoms f p,onatoms f q) | Iff(p,q) -> Iff(onatoms f p,onatoms f q) | Forall(x,p) -> Forall(x,onatoms f p) | Exists(x,p) -> Exists(x,onatoms f p) | _ -> fm;; let rec overatoms f fm b = match fm with Atom(a) -> f a b 96 AP´ ENDICE A. C ´ ODIGO START_INTERACTIVE;; filter (non trivial) (purednf <<(p \/ q /\ r) /\ ( ˜p \/ ˜r)>>);; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Simplificaci´ on. *) (* ------------------------------------------------------------------------- *) let psubst subfn = onatoms (fun p -> tryapplyd subfn p (Atom p));; let simpdnf fm = if fm = False then [] else if fm = True then [[]] else let djs = filter (non trivial) (purednf(nnf fm)) in filter (fun d -> not(exists (fun d’ -> psubset d’ d) djs)) djs;; (* ------------------------------------------------------------------------- *) (* Representaci´ on como f´ ormulas. *) (* ------------------------------------------------------------------------- *) let dnf fm = list_disj(map list_conj (simpdnf fm));; (* ------------------------------------------------------------------------- *) (* Ejemplo. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; let fm = <<(p \/ q /\ r) /\ (˜p \/ ˜r)>>;; dnf fm;; tautology(Iff(fm,dnf fm));; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Forma normal conjuntiva usando DNF. *) (* ------------------------------------------------------------------------- *) let purecnf fm = image (image negate) (purednf(nnf(Not fm)));; let simpcnf fm = if fm = False then [[]] else if fm = True then [] else let cjs = filter (non trivial) (purecnf fm) in filter (fun c -> not(exists (fun c’ -> psubset c’ c) cjs)) cjs;; let cnf fm = list_conj(map list_disj (simpcnf fm));; (* ------------------------------------------------------------------------- *) (* Example. *) 97 (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; let fm = <<(p \/ q /\ r) /\ (˜p \/ ˜r)>>;; cnf fm;; tautology(Iff(fm,cnf fm));; END_INTERACTIVE;; (* ========================================================================= *) (* FNC usando abreviaciones. *) (* ========================================================================= *) let mkprop n = Atom(P("p_"ˆ(string_of_num n))),n +/ Int 1;; (* ------------------------------------------------------------------------- *) (* N´ ucleo del procedimiento. *) (* ------------------------------------------------------------------------- *) let rec maincnf (fm,defs,n as trip) = match fm with And(p,q) -> defstep mk_and (p,q) trip | Or(p,q) -> defstep mk_or (p,q) trip | Iff(p,q) -> defstep mk_iff (p,q) trip | _ -> trip and defstep op (p,q) (fm,defs,n) = let fm1,defs1,n1 = maincnf (p,defs,n) in let fm2,defs2,n2 = maincnf (q,defs1,n1) in let fm’ = op fm1 fm2 in try (fst(apply defs2 fm’),defs2,n2) with Failure _ -> let v,n3 = mkprop n2 in (v,(fm’|->(v,Iff(v,fm’))) defs2,n3);; (* ------------------------------------------------------------------------- *) (* Funci´ on sobre el ´ ındice. *) (* ------------------------------------------------------------------------- *) let max_varindex pfx = let m = String.length pfx in fun s n -> let l = String.length s in if l <= m or String.sub s 0 m <> pfx then n else let s’ = String.sub s m (l - m) in if forall numeric (explode s’) then max_num n (num_of_string s’) else n;; 98 AP´ ENDICE A. C ´ ODIGO (* ------------------------------------------------------------------------- *) (* Procedimiento completo. *) (* ------------------------------------------------------------------------- *) let mk_defcnf fn fm = let fm’ = nenf fm in let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm’ (Int 0) in let (fm’’,defs,_) = fn (fm’,undefined,n) in let deflist = map (snd ** snd) (graph defs) in unions(simpcnf fm’’ :: map simpcnf deflist);; let defcnf fm = list_conj(map list_disj(mk_defcnf maincnf fm));; (* ------------------------------------------------------------------------- *) (* Ejemplo. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; defcnf <<(p \/ (q /\ ˜r)) /\ s>>;; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Optimizaci´ on del procedimiento. *) (* ------------------------------------------------------------------------- *) let subcnf sfn op (p,q) (fm,defs,n) = let fm1,defs1,n1 = sfn(p,defs,n) in let fm2,defs2,n2 = sfn(q,defs1,n1) in (op fm1 fm2,defs2,n2);; let rec orcnf (fm,defs,n as trip) = match fm with Or(p,q) -> subcnf orcnf mk_or (p,q) trip | _ -> maincnf trip;; let rec andcnf (fm,defs,n as trip) = match fm with And(p,q) -> subcnf andcnf mk_and (p,q) trip | _ -> orcnf trip;; let defcnfs fm = mk_defcnf andcnf fm;; let defcnf fm = list_conj (map list_disj (defcnfs fm));; (* ------------------------------------------------------------------------- *) (* Ejemplos. *) 99 (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; defcnf <<(p \/ (q /\ ˜r)) /\ s>>;; END_INTERACTIVE;; (* ========================================================================= *) (* Los procedimientos DP y DPLL. *) (* ========================================================================= *) (* ------------------------------------------------------------------------- *) (* El procedimiento DP. *) (* ------------------------------------------------------------------------- *) let one_literal_rule clauses = let u = hd (find (fun cl -> length cl = 1) clauses) in let u’ = negate u in let clauses1 = filter (fun cl -> not (mem u cl)) clauses in image (fun cl -> subtract cl [u’]) clauses1;; let affirmative_negative_rule clauses = let neg’,pos = partition negative (unions clauses) in let neg = image negate neg’ in let pos_only = subtract pos neg and neg_only = subtract neg pos in let pure = union pos_only (image negate neg_only) in if pure = [] then failwith "affirmative_negative_rule" else filter (fun cl -> intersect cl pure = []) clauses;; let resolve_on p clauses = let p’ = negate p and pos,notpos = partition (mem p) clauses in let neg,other = partition (mem p’) notpos in let pos’ = image (filter (fun l -> l <> p)) pos and neg’ = image (filter (fun l -> l <> p’)) neg in let res0 = allpairs union pos’ neg’ in union other (filter (non trivial) res0);; let resolution_blowup cls l = let m = length(filter (mem l) cls) and n = length(filter (mem (negate l)) cls) in m*n-m-n;; let resolution_rule clauses = let pvs = filter positive (unions clauses) in let p = minimize (resolution_blowup clauses) pvs in resolve_on p clauses;; 100 AP´ ENDICE A. C ´ ODIGO (* ------------------------------------------------------------------------- *) (* Procedimiento completo. *) (* ------------------------------------------------------------------------- *) let rec dp clauses = if clauses = [] then true else if mem [] clauses then false else try dp (one_literal_rule clauses) with Failure _ -> try dp (affirmative_negative_rule clauses) with Failure _ -> dp(resolution_rule clauses);; (* ------------------------------------------------------------------------- *) (* Satisfacibilidad y tautolog´ ıa usando DP. *) (* ------------------------------------------------------------------------- *) let dpsat fm = dp(defcnfs fm);; let dptaut fm = not(dpsat(Not fm));; (* ------------------------------------------------------------------------- *) (* Ejemplos. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; tautology <<(p \/ (q /\ ˜r)) /\ s>>;; dptaut <<(p \/ (q /\ ˜r)) /\ s>>;; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Procedimiento DPLL. *) (* ------------------------------------------------------------------------- *) let posneg_count cls l = let m = length(filter (mem l) cls) and n = length(filter (mem (negate l)) cls) in m + n;; let rec dpll clauses = if clauses = [] then true else if mem [] clauses then false else try dpll(one_literal_rule clauses) with Failure _ -> try dpll(affirmative_negative_rule clauses) with Failure _ -> let pvs = filter positive (unions clauses) in let p = maximize (posneg_count clauses) pvs in dpll (insert [p] clauses) or dpll (insert [negate p] clauses);; 101 let dpllsat fm = dpll(defcnfs fm);; let dplltaut fm = not(dpllsat(Not fm));; (* ------------------------------------------------------------------------- *) (* Ejemplo. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; dplltaut <<(p \/ (q /\ ˜r)) /\ s>>;; END_INTERACTIVE;; (* ========================================================================= *) (* L´ ogica de primer orden: sintaxis y sem´ antica. *) (* ========================================================================= *) (* ------------------------------------------------------------------------- *) (* T´ erminos. *) (* ------------------------------------------------------------------------- *) type term = Var of string | Fn of string * term list;; (* ------------------------------------------------------------------------- *) (* F´ ormula de primer orden. *) (* ------------------------------------------------------------------------- *) type fol = R of string * term list;; (* ------------------------------------------------------------------------- *) (* Parsing de t´ erminos. *) (* ------------------------------------------------------------------------- *) let is_const_name s = forall numeric (explode s) || s = "nil";; let rec parse_atomic_term vs inp = match inp with [] -> failwith "term expected" | "("::rest -> parse_bracketed (parse_term vs) ")" rest | "-"::rest -> papply (fun t -> Fn("-",[t])) (parse_atomic_term vs rest) | f::"("::")"::rest -> Fn(f,[]),rest | f::"("::rest -> papply (fun args -> Fn(f,args)) (parse_bracketed (parse_list "," (parse_term vs)) ")" rest) | a::rest -> 102 AP´ ENDICE A. C ´ ODIGO (if is_const_name a && not(mem a vs) then Fn(a,[]) else Var a),rest and parse_term vs inp = parse_right_infix "::" (fun (e1,e2) -> Fn("::",[e1;e2])) (parse_right_infix "+" (fun (e1,e2) -> Fn("+",[e1;e2])) (parse_left_infix "-" (fun (e1,e2) -> Fn("-",[e1;e2])) (parse_right_infix "*" (fun (e1,e2) -> Fn("*",[e1;e2])) (parse_left_infix "/" (fun (e1,e2) -> Fn("/",[e1;e2])) (parse_left_infix "ˆ" (fun (e1,e2) -> Fn("ˆ",[e1;e2])) (parse_atomic_term vs)))))) inp;; let parset = make_parser (parse_term []);; (* ------------------------------------------------------------------------- *) (* Parsing de f´ ormulas. *) (* ------------------------------------------------------------------------- *) let parse_infix_atom vs inp = let tm,rest = parse_term vs inp in if exists (nextin rest) ["="; "<"; "<="; ">"; ">="] then papply (fun tm’ -> Atom(R(hd rest,[tm;tm’]))) (parse_term vs (tl rest)) else failwith "";; let parse_atom vs inp = try parse_infix_atom vs inp with Failure _ -> match inp with | p::"("::")"::rest -> Atom(R(p,[])),rest | p::"("::rest -> papply (fun args -> Atom(R(p,args))) (parse_bracketed (parse_list "," (parse_term vs)) ")" rest) | p::rest when p <> "(" -> Atom(R(p,[])),rest | _ -> failwith "parse_atom";; let parse = make_parser (parse_formula (parse_infix_atom,parse_atom) []);; let default_parser = parse;; let secondary_parser = parset;; (* ------------------------------------------------------------------------- *) (* Printing de t´ erminos. *) (* ------------------------------------------------------------------------- *) let rec print_term prec fm = 103 match fm with Var x -> print_string x | Fn("ˆ",[tm1;tm2]) -> print_infix_term true prec 24 "ˆ" tm1 tm2 | Fn("/",[tm1;tm2]) -> print_infix_term true prec 22 " /" tm1 tm2 | Fn("*",[tm1;tm2]) -> print_infix_term false prec 20 " *" tm1 tm2 | Fn("-",[tm1;tm2]) -> print_infix_term true prec 18 " -" tm1 tm2 | Fn("+",[tm1;tm2]) -> print_infix_term false prec 16 " +" tm1 tm2 | Fn("::",[tm1;tm2]) -> print_infix_term false prec 14 "::" tm1 tm2 | Fn(f,args) -> print_fargs f args and print_fargs f args = print_string f; if args = [] then () else (print_string "("; open_box 0; print_term 0 (hd args); print_break 0 0; do_list (fun t -> print_string ","; print_break 0 0; print_term 0 t) (tl args); close_box(); print_string ")") and print_infix_term isleft oldprec newprec sym p q = if oldprec > newprec then (print_string "("; open_box 0) else (); print_term (if isleft then newprec else newprec+1) p; print_string sym; print_break (if String.sub sym 0 1 = " " then 1 else 0) 0; print_term (if isleft then newprec+1 else newprec) q; if oldprec > newprec then (close_box(); print_string ")") else ();; let printert tm = open_box 0; print_string "<<|"; open_box 0; print_term 0 tm; close_box(); print_string "|>>"; close_box();; #install_printer printert;; (* ------------------------------------------------------------------------- *) (* Printing de f´ ormulas. *) (* ------------------------------------------------------------------------- *) let print_atom prec (R(p,args)) = if mem p ["="; "<"; "<="; ">"; ">="] & length args = 2 then print_infix_term false 12 12 (" "ˆp) (el 0 args) (el 1 args) else print_fargs p args;; let print_fol_formula = print_qformula print_atom;; 104 AP´ ENDICE A. C ´ ODIGO #install_printer print_fol_formula;; (* ------------------------------------------------------------------------- *) (* Variables libres en t´ erminos y f´ ormulas. *) (* ------------------------------------------------------------------------- *) let rec fvt tm = match tm with Var x -> [x] | Fn(f,args) -> unions (map fvt args);; let rec var fm = match fm with False | True -> [] | Atom(R(p,args)) -> unions (map fvt args) | Not(p) -> var p | And(p,q) | Or(p,q) | Imp(p,q) | Iff(p,q) -> union (var p) (var q) | Forall(x,p) | Exists(x,p) -> insert x (var p);; let rec fv fm = match fm with False | True -> [] | Atom(R(p,args)) -> unions (map fvt args) | Not(p) -> fv p | And(p,q) | Or(p,q) | Imp(p,q) | Iff(p,q) -> union (fv p) (fv q) | Forall(x,p) | Exists(x,p) -> subtract (fv p) [x];; (* ------------------------------------------------------------------------- *) (* Ejemplos. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; <<(forall x. x < 2 ==> 2 * x <= 3) \/ false>>;; <<forall x y. exists z. x < z /\ y < z>>;; << ˜(forall x. P(x)) <=> exists y. ˜P(y)>>;; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Sem´ antica. *) (* ------------------------------------------------------------------------- *) let rec termval (domain,func,pred as m) v tm = match tm with 105 Var(x) -> apply v x | Fn(f,args) -> func f (map (termval m v) args);; let rec holds (domain,func,pred as m) v fm = match fm with False -> false | True -> true | Atom(R(r,args)) -> pred r (map (termval m v) args) | Not(p) -> not(holds m v p) | And(p,q) -> (holds m v p) & (holds m v q) | Or(p,q) -> (holds m v p) or (holds m v q) | Imp(p,q) -> not(holds m v p) or (holds m v q) | Iff(p,q) -> (holds m v p = holds m v q) | Forall(x,p) -> forall (fun a -> holds m ((x |-> a) v) p) domain | Exists(x,p) -> exists (fun a -> holds m ((x |-> a) v) p) domain;; (* ------------------------------------------------------------------------- *) (* Examples de interpretaciones particulares. *) (* ------------------------------------------------------------------------- *) let bool_interp = let func f args = match (f,args) with ("0",[]) -> false | ("1",[]) -> true | ("+",[x;y]) -> not(x = y) | ("*",[x;y]) -> x & y | _ -> failwith "uninterpreted function" and pred p args = match (p,args) with ("=",[x;y]) -> x = y | _ -> failwith "uninterpreted predicate" in ([false; true],func,pred);; START_INTERACTIVE;; holds bool_interp undefined <<forall x. (x = 0) \/ (x = 1)>>;; let fm = <<forall x. ˜(x = 0) ==> exists y. x * y = 1>>;; holds bool_interp undefined fm;; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Cierre universal de una f´ ormula. *) (* ------------------------------------------------------------------------- *) 112 AP´ ENDICE A. C ´ ODIGO | And(p,q) -> And(qelift vars p,qelift vars q) | Or(p,q) -> Or(qelift vars p,qelift vars q) | Imp(p,q) -> Imp(qelift vars p,qelift vars q) | Iff(p,q) -> Iff(qelift vars p,qelift vars q) | Forall(x,p) -> Not(qelift vars (Exists(x,Not p))) | Exists(x,p) -> let djs = disjuncts(nfn(qelift (x::vars) p)) in list_disj(map (qelim (qfn vars) x) djs) | _ -> fm in fun fm -> simplify(qelift (fv fm) (miniscope fm));; let cnnf lfn = let rec cnnf fm = match fm with And(p,q) -> And(cnnf p,cnnf q) | Or(p,q) -> Or(cnnf p,cnnf q) | Imp(p,q) -> Or(cnnf(Not p),cnnf q) | Iff(p,q) -> Or(And(cnnf p,cnnf q),And(cnnf(Not p),cnnf(Not q))) | Not(Not p) -> cnnf p | Not(And(p,q)) -> Or(cnnf(Not p),cnnf(Not q)) | Not(Or(And(p,q),And(p’,r))) when p’ = negate p -> Or(cnnf (And(p,Not q)),cnnf (And(p’,Not r))) | Not(Or(p,q)) -> And(cnnf(Not p),cnnf(Not q)) | Not(Imp(p,q)) -> And(cnnf p,cnnf(Not q)) | Not(Iff(p,q)) -> Or(And(cnnf p,cnnf(Not q)), And(cnnf(Not p),cnnf q)) | _ -> lfn fm in simplify ** cnnf ** simplify;; (* ------------------------------------------------------------------------- *) (* Igualdad. *) (* ------------------------------------------------------------------------- *) let is_eq = function (Atom(R("=",_))) -> true | _ -> false;; let dest_eq fm = match fm with Atom(R("=",[s;t])) -> s,t | _ -> failwith "dest_eq: not an equation";; (* ------------------------------------------------------------------------- *) (* ´ Ordenes lineales densos. *) (* ------------------------------------------------------------------------- *) let afn_dlo vars fm = match fm with 113 Atom(R("<=",[s;t])) -> Not(Atom(R("<",[t;s]))) | Atom(R(">=",[s;t])) -> Not(Atom(R("<",[s;t]))) | Atom(R(">",[s;t])) -> Atom(R("<",[t;s])) | _ -> fm;; let lfn_dlo fm = match fm with Not(Atom(R("<",[s;t]))) -> Or(Atom(R("=",[s;t])),Atom(R("<",[t;s]))) | Not(Atom(R("=",[s;t]))) -> Or(Atom(R("<",[s;t])),Atom(R("<",[t;s]))) | _ -> fm;; let dlobasic fm = match fm with Exists(x,p) -> let cjs = subtract (conjuncts p) [Atom(R("=",[Var x;Var x]))] in try let eqn = find is_eq cjs in let s,t = dest_eq eqn in let y = if s = Var x then t else s in list_conj(map (subst (x |=> y)) (subtract cjs [eqn])) with Failure _ -> if mem (Atom(R("<",[Var x;Var x]))) cjs then False else let lefts,rights = partition (fun (Atom(R("<",[s;t]))) -> t = Var x) cjs in let ls = map (fun (Atom(R("<",[l;_]))) -> l) lefts and rs = map (fun (Atom(R("<",[_;r]))) -> r) rights in list_conj(allpairs (fun l r -> Atom(R("<",[l;r]))) ls rs) | _ -> failwith "dlobasic";; let quelim_dlo = lift_qelim afn_dlo (dnf ** cnnf lfn_dlo) (fun v -> dlobasic);; (* ------------------------------------------------------------------------- *) (* Ejemplos. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; quelim_dlo <<exists z. z < x /\ z < y>>;; quelim_dlo <<exists z. x < z /\ z < y>>;; quelim_dlo <<(forall x. x < a ==> x < b)>>;; quelim_dlo <<forall a b. (forall x. x < a ==> x < b) <=> a <= b>>;; END_INTERACTIVE;;