Articulo de referencia

FO(.)

En informática , FO(.) (también conocido como FO-dot ) es un lenguaje de representación del conocimiento basado en lógica de primer orden (FO). [ 1 ] Extiende FO con tipos , agr...

En informática , FO(.) (también conocido como FO-dot ) es un lenguaje de representación del conocimiento basado en lógica de primer orden (FO). [ 1 ] Extiende FO con tipos , agregados (conteo, suma, maximización... sobre un conjunto), aritmética, definiciones inductivas, funciones parciales y objetos intensionales.

Por sí sola, una base de conocimiento FO(.) no puede ejecutarse, ya que es solo una "bolsa de información" que se utiliza como entrada para varios algoritmos de razonamiento genéricos. Los motores de razonamiento que utilizan FO(.) incluyen IDP-Z3, [ 2 ] IDP [ 3 ] [ 4 ] y FOLASP. [ 5 ] Como ejemplo, el sistema IDP permite generar modelos , responder consultas de conjuntos, comprobar la implicación entre dos teorías y comprobar la satisfacibilidad , entre otros tipos de inferencia sobre una base de conocimiento FO(.).

FO(.) tiene cuatro tipos de sentencias:

  • Declaraciones de tipos, funciones y predicados,
  • Axiomas , es decir, enunciados lógicos sobre mundos posibles,
  • Definiciones que especifican una interpretación única de un símbolo definido, dada la interpretación de sus parámetros. Las definiciones pueden ser inductivas.
  • Enumeraciones, es decir, definiciones de símbolos mediante enumeración.

Ejemplo

Una ley electoral especifica que los ciudadanos deben tener al menos 18 años para votar. Además, si la ley electoral se interpreta como prescriptiva, votar es obligatorio cuando se es mayor de 18 años. Esto se puede representar en FO(.) de la siguiente manera:

vocabulario V { edad: () → ℤ // declaración de función prescriptivo, voto: () → 𝔹 // declaraciones de predicados } teoría T:V { edad() < 18 ⇒ ¬votar(). // axioma: si eres menor de 18 años, no puedes votar. prescriptivo() ⇒ (edad() ≥ 18 ⇒ votar()). // axioma: si es prescriptivo: si tienes al menos 18 años, debes votar } 

En este código, A B indica una función de A a B ,Z{\displaystyle \mathbb {Z} }denota números enteros ,B{\displaystyle \mathbb {B} }denota los booleanos , ¬denota la negación y denota el condicional material . Los predicados < y ≥ están incorporados y tienen su significado habitual.

Dicha base de conocimientos puede convertirse automáticamente en un Abogado Interactivo [ 6 ] (ver aquí [ 7 ] ).

Referencias

  1. Denecker, Marc (2000). "Extending classical logic with inductive definitions". International Conference on Computational Logic : 703– 717. arXiv : cs/0003019 . Bibcode : 2000cs........3019D .
  2. "IDP-Z3" . Consultado el 1 de febrero de 2022 .
  3. De Cat, Broes; Bogaerts, Bart; Bruynooghe, Maurice; Janssens, Gerda; Denecker, Marc (2018). «La lógica de predicados como lenguaje de modelado: El sistema IDP» . Programación lógica declarativa: Teoría, sistemas y aplicaciones . pp. 279–323 . doi : 10.1145/3191315.3191321 . ISBN  9781970001990. S2CID 3866665 . 
  4. "IDP" . Consultado el 1 de febrero de 2022 .
  5. "FOLASP" . Consultado el 1 de febrero de 2022 .
  6. "Consultor interactivo" . Consultado el 1 de febrero de 2022 .
  7. "Abogado interactivo" . Consultado el 1 de febrero de 2022 .
  • Sitio web oficial