Formas normales de fórmulas lógicas PDF

Preview

Summary

Se explican las distintas formas normales de la lógica de proposiciones y predicados y la forma en la que éstas se obtienen....

Description

Formas normales 10 de noviembre de 2018

Índice 1 Formas normales en lógica de proposiciones 1.1 Definiciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Método de transformación . . . . . . . . . . . . . . . . . . . . . . . . . . .

1 2 2

2 Formas normales en lógica de predicados 2.1 Forma normal de prenexa . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.1 Método de transformación . . . . . . . . . . . . . . . . . . . . . . 2.2 Forma normal de Skolem . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5 5 5 7

A menudo es necesario transformar una fórmula en otra, sobre todo transformar una fórmula a su «forma normal». Esto se consigue transformando la fórmula en otra equivalente y repitiendo el proceso hasta conseguir la forma deseada. En estos apuntes 1 se dan las reglas necesarias para transformar sintácticamente una fórmula en una forma normal más adecuada para la demostración automática y que conserva la semántica de la fórmula original. Por ejemplo se pueden usar estas reglas para derivar la fórmula  a partir de otra dada, comprobando así la inconsistencia de la fórmula original.

1.

Formas normales en lógica de proposiciones

Gracias a las leyes asociativas (ver Cuadro 1) los paréntesis en (F ∨ (G ∨ H)) o en ((F ∨ G) ∨ H ) pueden eliminarse, es decir, se puede escribir (F ∨ G ∨ H). En general se va a poder escribir sin ambigüedad una fórmula D = (F1 ∨ F2 ∨ . . . ∨ Fn ) donde F1 , F2 , . . . , Fn son fórmulas. La fórmula D es cierta cuando lo es al menos una de las Fi , en caso contrario D es falsa. La fórmula D recibe el nombre de disyunción de las fórmulas F1 , F2 , . . . , Fn . De modo análogo se puede escribir C = (F1 ∧ F2 ∧ ... ∧ Fn ) que es cierta cuando lo son F1 , F2 , . . . , Fn , si alguna de las Fi es falsa también lo es C. La fórmula C se llama conjunción de F1 , F2 , . . . , Fn . El orden en que aparecen los Fi es indiferente debido a la ley conmutativa (ver Cuadro 1). 1

Proceden en su mayor parte de la traducción de partes seleccionadas del capítulo 3 de C [ R73], y en menor medida del capítulo 2 de [LVDG91].

Formas normales

1.1

Definiciones

1.1. Definiciones Ahora se pueden definir las formas normales como sigue: Definición 1(Literal, literales complementarios, par complementario). Un literal es un átomo o la negación de un átomo. Si P, Q, R son átomos P , ¬P , Q, ¬Q, R, ¬R son literales. Dos literales l y l′ se dicen que son literales complementarios si y sólo si l = ¬l′ . Al conjunto {l, ¬l′ } se le llama par complementario. Definición 2 (Forma normal disyuntiva) . Una fórmula F se dice que está en forma normal disyuntiva si y sólo si F es de la forma F = (F1 ∨ F2 ∨ . . . Fn ) , donde cada Fi es una conjunción de literales. Definición 3 (Forma normal conjuntiva) . Una fórmula F se dice que está en forma normal conjuntiva si y sólo si F es de la forma F = (F1 ∧ F2 ∧ . . . ∧ Fn ), donde cada Fi es una disyunción de literales. Definición 4(Cláusula, cláusula unitaria, cláusula vacía). Una cláusula es una disyunción de cero o más literales. A veces se utiliza un conjunto de literales como equivalente a una cláusula suponiendo la disyunción entre los literales del conjunto. Así se tiene, por ejemplo, que P ∨ Q ∨ ¬R = {P, Q, ¬R}. Cuando la cláusula tiene un único literal se llama cláusula unitaria. Cuando no contiene ningún literal cláusula vacía . Como la cláusula vacía no tiene ningún literal, no puede ser satisfecha por ninguna interpretación. La cláusula vacía es siempre falsa y se representa, al igual que la fórmula siempre falsa, por el símbolo . Definición 5 (Forma clausulada). Una forma clausulada es un conjunto de cláusulas entre las que se supone la conjunción.

Ejemplo 1.1. Dados los átomos P , Q y R, la fórmula (¬P ∧ Q) ∨ (P ∧ ¬Q ∧ ¬R) es una fórmula en forma normal disyuntiva,(P ∨ ¬Q ∨ R) ∧ (¬P ∨ Q) es una fórmula en forma normal conjuntiva, y{P ∨ ¬Q ∨ R, ¬P ∨ Q} es la forma clausulada de la fórmula anterior. {{P, ¬Q, R}, {¬P, Q}} es otra forma de poner la forma clausulada. Cualquier fórmula se puede transformar en una forma normal. Esta transformación se lleva a cabo mediante la aplicación de las leyes del Cuadro 1. El procedimiento es el siguiente.

1.2. Método de transformación Paso 1: Usar las leyes: (L1) F ↔ G = (F → G) ∧ (G → F ) y (L2) F → G = ¬F ∨ G para eliminar las conectivas lógicas ↔ y →. Paso 2: Usar repetidamente la ley (L10) ¬(¬F ) = F y las leyes de De Morgan: (L11.a) ¬(F ∧ H) = ¬F ∨ ¬G y (L11.b) ¬(F ∨ H) = ¬F ∧ ¬G para disminuir el alcance de la negación a un único literal.

César Ignacio García Osorio

2

LSI – Univ. de Burgos

Formas normales

(L1) Eliminación del bicondicional (L2) Eliminación del condicional (L3) Conmutativa (L4) Asociativa (L5) Distributiva (L6) Absorción (L7) Contradicción (L8) Exclusión de los medios (L9) Idempotencia (L10) Doble negación (L11) De Morgan (L12) (L13) De Morgan para cuantificadores (L14) Distributiva de cuantificadores (L15)

1.2

Método de transformación

(a) (b ) F ↔ G ≡ (F → G) ∧ (G → F ) F → G ≡ ¬F ∨ G F ∨G≡ G∨F (F ∨ G) ∨ H ≡ F ∨ (G ∨ H) F ∨ (G ∧ H) ≡ (F ∨ G) ∧ (F ∨ H) F ∨≡F F ∨≡ F ∨ ¬F ≡ 

F ∧G≡ G∧F (F ∧ G) ∧ H ≡ F ∧ (G ∧ H) F ∧ (G ∨ H) ≡ (F ∧ G) ∨ (F ∧ H ) F ∧≡F F ∧≡ F ∧ ¬F ≡ 

F ∨F ≡F

F ∧F ≡F ¬(¬F ) ≡ F ¬(F ∨ H) ≡ ¬F ∧ ¬G ¬(F ∧ H) ≡ ¬F ∨ ¬G G ∨ (Qx)F [x] ≡ (Qx)(G ∨ F [x]) ¬(∀x)F [x] ≡ (∃x)(¬F [x])

G ∧ (Qx)F [x] ≡ (Qx)(G ∧ F [x]) ¬(∃x)F [x] ≡ (∀x)(¬F [x])

(∀x)F [x] ∧ (∀x)H[x] ≡ (∀x)(F [x] ∧ H[x]) (Q1 x)F [x] ∨ (Q2 x)H[x] ≡ (Q1 x)(Q2 z )(F [x] ∨ H [z])

(∃x)F [x] ∨ (∃x)H [x] ≡ (∃x)(F [x] ∨ H[x]) (Q3 x)F [x] ∧ (Q4 x)H[x] ≡ (Q3 x)(Q4 z )(F [x] ∧ H [z ])

Cuadro 1: Leyes de equivalencia

César Ignacio García Osorio

3

LSI – Univ. de Burgos

Formas normales

1.2

Método de transformación

Paso 3: Usar de forma repetida las leyes distributivas: (L5.a) F ∧(G∨H) = (F ∧G)∨(F ∧H) y (L5.b) F ∨ (G ∧ H) = (F ∨ G) ∧ (F ∨ H) y las otras leyes para obtener la forma normal.

Ejemplo 1.2. Obtener la forma normal conjuntiva de la fórmula (P ∧ (Q → R)) → S . (P = = = = = = = = =

∧ (Q → R)) → S (P ∧ (¬Q ∨ R)) → S ¬(P ∧ (¬Q ∨ R)) ∨ S (¬P ∨ ¬(¬Q ∨ R)) ∨ S (¬P ∨ (¬(¬Q) ∧ ¬R)) ∨ S (¬P ∨ (Q ∧ ¬R)) ∨ S ((¬P ∨ Q) ∧ (¬P ∨ ¬R)) ∨ S S ∨ ((¬P ∨ Q) ∧ (¬P ∨ ¬R)) (S ∨ ((¬P ∨ Q)) ∧ (S ∨ (¬P ∨ ¬R)) (S ∨ ¬P ∨ Q) ∧ (S ∨ ¬P ∨ ¬R)

por L2 por L2 por L11.b por L11.a por L10 por L5.a por L3.a por L5.a por L4

Por tanto una forma normal conjuntiva de(P ∧ (Q → R)) → S es (S ∨ ¬P ∨ Q) ∧ (S ∨ ¬P ∨ ¬R) la forma clausulada para esta fórmula será: {{S, ¬P, Q}, {S, ¬P, ¬R}}.

Ejemplo 1.3. Dadas las fórmulas:F1 = (P → Q), F2 = ¬Q, G = ¬P. Demostrar que G es consecuencia lógica deF1 y F2 . Esto se podría hacer mediante el uso de tablas de verdad para comprobar que todo modelo de F1 y de F2 es también modelo de G. Pero se puede hacer también usando los resultados del teorema de refutación en combinación con el procedimiento de normalización de una fórmula. Usando el punto 2 del citado teorema y llevando la fórmula (((P → Q) ∧ ¬Q) → ¬P ) a forma normal conjuntiva, tenemos: (((P → Q) ∧ ¬Q) → ¬P ) = ¬((P → Q) ∧ ¬Q) ∨ ¬P = ¬((¬P ∨ Q) ∧ ¬Q) ∨ ¬P = ¬((¬P ∧ ¬Q) ∨ (Q ∧ ¬Q)) ∨ ¬P = ¬((¬P ∧ ¬Q) ∨ ) ∨ ¬P = ¬((¬P ∧ ¬Q)) ∨ ¬P = (P ∨ Q) ∨ ¬P = (Q ∨ P ) ∨ ¬P = Q ∨ (P ∨ ¬P ) = Q∨ = 

por L2 por L2 por L5.b por L8.b por L6.a por L11.b por L3.a por L4.a por L8.a por L7.a

Como la fórmula (((P → Q) ∧ ¬Q) → ¬P ) es válida (ya que es equivalente a que es cierta para todo modelo), podemos concluir que G es consecuencia lógica de F1 y F2 . También ysando el punto 3 del citado teorema de refutación y transformando((P → Q) ∧ ¬Q ∧ P ) a forma normal disyuntiva, tenemos:

César Ignacio García Osorio

4

LSI – Univ. de Burgos

Formas normales ((P = = = =

→ Q) ∧ ¬Q ∧ P ) (¬P ∨ Q) ∧ ¬Q ∧ P (¬P ∧ ¬Q ∧ P ) ∨ (Q ∧ ¬Q ∧ P ) ∨ 

por L2 por L5.b por L8.b por L6.a

Como la fórmula ((P → Q) ∧ ¬Q ∧ P ) es inconsistente (ya que es equivalente a que siempre es falsa), de nuevo podemos concluir que G es consecuencia lógica de F1 y F2 .

En el ejemplo anterior se ha mostrado que la conclusión ( G ) se sigue de unos hechos dados (F1 y F2 ), llamados axiomas . La demostración de que la conclusión se sigue de los axiomas se llama prueba. Un procedimiento para encontrar una prueba se llama procedimiento de prueba. .

2.

Formas normales en lógica de predicados

Al igual que en la lógica proposicional, en la lógica de predicados también existen formas normales. Un primer paso en la obtención de la forma normal más adecuada para los procedimientos de deducción automática es llevar todos los cuantificadores a la parte izquierda de la fórmula: forma normal prenexa , a continuación se transforma la parte de la fórmula sin cuantificadores a la forma normal conjuntiva , de un modo análogo al visto para la lógica de proposiciones, por último, se eliminan los cuantificadores universales para obtener la forma normal de Skolem . Ahora, todos los cuantificadores son universales. Podemos representar la fórmula como un conjunto de cláusulas siempre y cuando tengamos presente la mencionada cuantificación universal de las variables.

2.1. Forma normal de prenexa Definición 6 (Forma normal prenexa) . Una fórmula F de la lógica de predicados se dice que está en forma normal prenexa si y sólo si la F tiene la forma: (Q1 x1 )(Q2 x2 ) · · · (Qn xn )M[x1 , x2 , . . . , xn ] Donde los Qi son cuantificadores: o bien ∃ o bien ∀, y M[x1 , x2 , . . . , xn ] es una fórmula que no contiene cuantificadores cuyas únicas variables (que son libres) son x1 , x2 , . . . , xn. (Q1 x1 )(Q2 x2 ) · · · (Qn xn ) se llama prefijo y a M se le llama matriz de la fórmula F . 2.1.1. Método de transformación Transformación de una fórmula a su forma normal prenexa. Paso 1: Usar las leyes (L1) (L2)

F ↔ G = (F → G) ∧ (G → F ) y F → G = ¬F ∨ G

para eliminar las conectivas lógicas ↔ y →.

César Ignacio García Osorio

5

LSI – Univ. de Burgos

Formas normales

2.1

Forma normal de prenexa

Paso 2: Usar repetidamente: la ley de doble negación (L10) ¬(¬F ) = F , las leyes de De Morgan: (L11.a) ¬(F ∨ H) = ¬F ∧ ¬G y (L11.b) ¬(F ∧ H) = ¬F ∨ ¬G, y las leyes de De Morgan para cuantificadores: (L13.a) ¬(∀x)F [x] = (∃x)(¬F [x]) y (L13.b) ¬((∃x)F [x]) = (∀x)(¬F [x]) para llevar los signos de negación inmediatamente delante de los átomos. Paso 3: Renombrar las variables ligadas si fuese necesario (para poder aplicar las leyes L15). Paso 4: Usar las leyes: (L12.a) (L12.b) (L14.a) (L14.b) (L15.a) (L15.b)

G ∨ (Qx)F [x] = (Qx)(G ∨ F [x]), G ∧ (Qx)F [x] = (Qx)(G ∧ F [x]), (∀x)F [x] ∧ (∀x)H[x] = (∀x)(F [x] ∧ H [x]), (∃x)F [x] ∨ (∃x)H[x] = (∃x)(F [x] ∨ H [x]), (Q1 x)F [x] ∨ (Q2 x)H[x] = (Q1 x)(Q2 z )(F [x] ∨ H[z]) y (Q3 x)F [x] ∧ (Q4 x)H[x] = (Q3 x)(Q4 z )(F [x] ∧ H[z])

para mover los cuantificadores a la izquierda de la fórmula para obtener la forma normal prenexa2 .

Ejemplo 2.1. Obtener la forma normal prenexa de la fórmula: (∀x)(∀y)((∃z)P (x, y, z) ∨ ((∃u)Q(x, u) → (∃v)Q(y, v))), se procede como sigue: (∀x)(∀y)((∃z )P (x, y, z) ∨ ((∃u)Q(x, u) → (∃v)Q(y, v))) = (∀x)(∀y)((∃z)P (x, y, z) ∨ (¬(∃u)Q(x, u) ∨ (∃v)Q(y, v))) = (∀x)(∀y)((∃z )P (x, y, z) ∨ ((∀u)¬Q(x, u) ∨ (∃v)Q(y, v))) = (∀x)(∀y)(∃z )(∀u)(∃v)(P (x, y, z) ∨ ¬Q(x, u) ∨ Q(y, v))

por L2 por L13.b usando L12

La forma normal prenexa es uno de los pasos que hay que seguir para poder transformar una fórmula en una cláusula, es decir, una fórmula cerrada de la forma: (∀x1 ) · · · (∀xs )(L1 ∨ · · · ∨ Lm ) donde cada Li , i = 1, . . . , m, m ≥ 0 , es un literal con Li 6= Lj para cada i 6= j, y x1 , . . . , xs , s ≥ 0, son variables que ocurren en (L1 ∨ · · · ∨ Lm ).

2

En este último paso, es conveniente que los cuantificadores existenciales queden lo más a la izquierda posible. Los motivos de esto se verán en la sección siguiente (cuando se introduzca el concepto de funciones de Skolem).

César Ignacio García Osorio

6

LSI – Univ. de Burgos

Formas normales

2.2

Forma normal de Skolem

2.2. Forma normal de Skolem En el proceso de llevar una fórmula bien formada a forma clausulada se llega a un punto en el que hay que eliminar los cuantificadores existenciales. Esto se consigue sustituyendo las variables cuantificadas existencialmente por las llamadas funciones de Skolem (cuando el cuantificador existencial aparece precedido de algún cuantificador universal) y constantes de Skolem (cuando el cuantificador existencial es el primero de la fórmula). En esta sección se explica la forma de proceder para hacer esto. Además, se enuncia y demuestra un importante teorema que relaciona la insatisfacibilidad de una fórmula bien formada con la de su forma normal de Skolem. Sea G una fórmula que ya está en forma normal prenexa (Q1 x1 )(Q2 x2 ) . . . (Qn xn )M[x1 , x2 , . . . , xn ] donde M[x1 , x2 , . . . , xn ] está en forma normal conjuntiva. Sea Qr un cuantificador existencial del prefijo (1 ≤ r ≤ n). Qr se elimina del prefijo y se realizan los siguientes cambios: (a) Si no hay ningún cuantificador universal delante de Qr • Elegir una constate c que no ocurra en M. • Reemplazar todas las ocurrencias de xr en M por c. (b) Sean Qs1 , Qs2 , . . . , Qsm todos los cuantificadores universales que aparecen delante de Qr con (1 ≤ s1 < s2 . . . sm < r ). • Elegir una función m-aria fr que no ocurra en M. • Reemplazar todas las ocurrencias de xr en M por fr (xs1 , xs1 . . . , xsm ). Cuando todos los cuantificadores existenciales han sido eliminados por este procedimiento, la última fórmula obtenida Gs es la forma estándar de Skolem de G. Las constantes y funciones utilizadas para reemplazar las variables cuantificadas existencialmente reciben el nombre de constantes de Skolem y funciones de Skolem.

Ejemplo 2.2. Obtener la forma estándar de Skolem de la fórmula: (∃x)(∀y)(∀z )(∃u)(∀v)(∃w)P (x, y, z, u, v, w) Como ya está en forma normal prenexa y la matriz en forma normal conjuntiva, simplemente tenemos que hacer las eliminaciones de cuantificadores existenciales. Como(∃x) no está precedido de ningún cuantificador universal, la variablex se sustituye por una constante, por ejemplo a. Como (∃u) está precedido por los cuantificadores universales sobre las variablesy y z la variable u se sustituye por la función f (y, z). Por último como (∃w) está precedido por los cuantificadores universales sobre las variablesy , z y v , se sustituirá por una función, como por ejemplo g(y, z, v). Con lo cual se obtiene: (∀y)(∀z )(∀v)P (a, y, z, f (y, z ), v, g (y, z, v))

César Ignacio García Osorio

7

LSI – Univ. de Burgos

Formas normales

2.2

Forma normal de Skolem

Ya se había introducido el concepto de cláusula como una disyunción de cero o más literales, también se ha visto que una cláusula podía representarse como un conjunto de literales entre los que se supone la disyunción. Del mismo modo, un conjunto de cláusulas S se puede ver como la conjunción de todas las cláusulas en S, donde cada variable en S se considera que está gobernada por un cuantificador universal. Como ya se ha dicho, los cuantificadores existenciales pueden ser eliminados sin afectar a la propiedad de inconsistencia. Esto es lo que nos dice el siguiente teorema. Teorema 1. Sea G una sentencia y Gs su forma estándar de Skolem. G es inconsistente si y sólo si Gs es inconsistente. DEMOSTR ACIÓN : Sin perdida de generalidad se puede suponer queG está en forma normal prenexa, es decir: G = (Q1 x1 )(Q2 x2 ) . . . (Qn xn )M [x1 , x2 , . . . , xn ] Sea Qr el primer cuantificador existencial de G y G1 igual a: G1 = (∀x1 ) . . . (∀xr−1 )(Qr+1 xr+1 ) . . . (Qn xn ) M [x1 , . . . , xr−1 , f (x1 , . . . , xr−1 ), xr+1 , . . . , xn ] con f la función de Skolem correspondiente a xr . Se va a demostrar queG es inconsistente si y sólo si G1 es inconsistente. El razonamiento será por reducción al absurdo. • G inconsistente ⇒ G1 inconsistente. Sea G inconsistente y supongamosG1 consistente. Por ser G1 consistente, existe una interpretación I tal que bajo esa interpretaciónG1 es cierta. Es decir, para todo x1 , . . . , xr−1 existe al menos un elemento del dominio,d r = f (x1 , . . . , xr−1 ), tal que la fórmula: (Qr+1 xr+1 ) . . . (Qn xn )M [x1 , . . . , xr−1 , d r , xr+1 , . . . , xn ] es cierta en I. Es decir, la fórmula: (Qr+1 xr+1 ) . . . (Qn xn )M [x1 , . . . , xr−1 , xr , xr+1 , . . . , xn ] es cierta en I para todo x1 , . . . , xr−1 y para algún xr (en concreto existe el xr = d r ). Esto es, G es cierto en I, lo que contradice la asunción de queG es inconsistente. Por tanto G1 no puede ser consistente. • G1 inconsistente ⇒ G inconsistente. Sea G1 inconsistente y supongamosG consistente, por ser G consistente, existe una interpretación I sobre un dominio D tal que G es cierta bajoI. Es decir, para todo x1 , . . . , xr−1 existe un elemento xr tal que la fórmula: (Qr+1 xr+1 ) . . . (Qn xn )M [x1 , . . . , xr−1 , xr , xr+1 , . . . , xn ] es cierta en I. Extendamos la interpretación I con una función f de aridad (r − 1) que vaya de (x1 , . . . , xr−1 ) a xr para todo x1 , . . . , xr−1 en D, es decir, tenemos que f (x1 , . . . , xr−1 ) = xr . Llamaremos I ′ a esta nueva interpretación. Con esta definición está claro que la sentencia: (Qr+1 xr+1 ) . . . (Qn xn )M [x1 , . . . , xr−1 , f (x1 , . . . , xr−1 ), xr+1 , . . . , xn ] es cierta en I ′ para todo x1 , . . . , xr−1 . Pero esto contradice la asunción de que G1 fuera inconsistente. Por tanto, G debe ser inconsistente.

César Ignacio García Osorio

8

LSI – Univ. de Burgos

Formas normales

Referencias

La demostración del teorema ya es inmediata, por inducción sobre el número total de cuantificadores existenciales. Sim es el número total de cuantificadores existenciales, hacemos G0 = G y Gk será la fórmula obtenida a partir deGk−1 reemplazando el primer cuantificador existencial por una función de Skolem parak = 1, 2, . . . , m. Claramente Gs = Gm. La demostración por inducción sobre Gi utiliza los mismos argumentos que el paso deG a G1 . Por tanto, se concluye que G es inconsistente si y sólo si Gs es inconsistente.

 Sea Gs la forma estándar de Skolem de una fórmula G. Si G es inconsistente, entonces por el Teorema 1, G ≡ Gs. Si G no es inconsistente, hay que hacer notar que en general G no es equivalente a Gs .

Ejemplo 2.3. Sea G = (∃x)P (x) y Gs = P (a). Claramente Gs es la forma estándar de Skolem de G. Sin embargo, para la interpretación I definida como: Dominio: D = {1, 2} Asignación para a: a 1 Asignación para P : P (1) F

P (2) T

claramente, G es cierta en I, pero Gs en falsa en I. Por tanto G 6≡ Gs .

Es evidente que una fórmula puede tener más de una forma normal de Skolem, por simplicidad cuando se transforma una fórmula G en su forma estándar Gs es conveniente reemplazar los cuantificadores existenciales por funciones de Skolem que sean lo más simples posibles, esto significa que tengan el menor número de variables posibles. Cuando se tiene una fórmula como F = F1 ∧ . . . ∧ Fn , se puede obtener el conjunto de cláusulas S que representa la forma estándar de Skolem de F hallando los conjuntos de cláusulas Si que representan las formas normales de Skolem de cada Fi y calculando la unión de los mismos. Se tiene que S = S1 ∪ . . . ∪ Sn . Usando argumentos similares a los dados en el teorema 1 no es difícil ver que F es inconsistente si y sólo si S es inconsistente.

Referencias [CR73]

Chin-Liang Chang and Char-Tung Lee Richard. Symbolic Logic and Mechanica...