Tarea QnA para Z3. ¿Es posible?

Estoy tratando de resolver una tarea de respuesta de preguntas. Hay varios enfoques para esto, como los métodos de aprendizaje profundo, la consulta de gráficos de conocimiento, la búsqueda semántica, etc. ¿Pero crees que sería posible utilizar el teorema probador Z3 para esa tarea también? Por ejemplo, si podemos presentar el conocimiento como un conjunto de axiomas, cada axioma consta de predicados (relaciones), sujetos y objetos, y se expresa en cláusulas FOL, entonces podemos atravesarlos y encontrar una respuesta a la consulta (que también puede ser expresada como un axioma). Por ejemplo, puedo codificar un conocimiento simple “el inglés es un idioma” en cláusulas FOL:

exist l. (language (l) & amp; amp; exists n. (name (n) & amp; amp;: op1 (n, & amp; quot; Inglés & amp; quot;) & amp; amp; : name (l, n))))

¿Cómo puedo traducir esto a Z3? ¿Y cómo puedo extraer una respuesta a la consulta “{desconocido} es lenguaje” para encontrar una variable o cláusula {desconocido}? Tenga en cuenta que {desconocido} puede ser cualquier cosa. Puede ser un átomo o una cláusula lógica según la coincidencia con la consulta.

davy.ai

June 5, 2023 at 6:18 pm

Para traducir la cláusula FOL “exists l.(language(l) & exists n.(name(n) & :op1(n,”English”) & :name(l,n)))” en Z3, primero necesitamos definir las variables relevantes y sus tipos. Podemos definir “l” como una variable con tipo “Language” y “n” como una variable con tipo “Name”. También necesitamos definir los predicados y funciones relevantes, como “language” y “name”.

En Z3, podemos usar el método “Exists” para expresar la existencia de estas variables y predicados, y usar el método “And” para combinarlos:

(declare-sort Language)
(declare-sort Name)

; Definir las funciones language y name
(declare-fun language (Language) Bool)
(declare-fun name (Name Language) Bool)

; Definir el idioma inglés
(declare-const eng Language)
(assert (language eng))
(assert (name "English" eng))

; Definir el axioma
(assert (Exists ((l Language) (n Name))
                (And (language l) (name n l) (= n "English"))))

Para extraer una respuesta a la consulta “{unknown} es lenguaje”, podemos definir de manera similar las variables y predicados relevantes y utilizar el método “Check-Sat” para verificar un modelo que satisfaga la consulta. Por ejemplo, si queremos encontrar una variable {unknown} que satisfaga la consulta, podemos escribir:

(declare-const unknown Language)
(assert (language unknown))
(check-sat)
(get-model)

Esto devolverá un modelo que asigna un valor a “unknown” que satisface la consulta. Si no se encuentra ningún modelo, significa que no hay variable que satisfaga la consulta.

Answer

davy.ai

June 5, 2023 at 6:18 pm
Para traducir la cláusula FOL “exists l.(language(l) & exists n.(name(n) & :op1(n,”English”) & :name(l,n)))” en Z3, primero necesitamos definir las variables relevantes y sus tipos. Podemos definir “l” como una variable con tipo “Language” y “n” como una variable con tipo “Name”. También necesitamos definir los predicados y funciones relevantes, como “language” y “name”.

En Z3, podemos usar el método “Exists” para expresar la existencia de estas variables y predicados, y usar el método “And” para combinarlos:
```
(declare-sort Language)
(declare-sort Name)

; Definir las funciones language y name
(declare-fun language (Language) Bool)
(declare-fun name (Name Language) Bool)

; Definir el idioma inglés
(declare-const eng Language)
(assert (language eng))
(assert (name "English" eng))

; Definir el axioma
(assert (Exists ((l Language) (n Name))
                (And (language l) (name n l) (= n "English"))))
```
Para extraer una respuesta a la consulta “{unknown} es lenguaje”, podemos definir de manera similar las variables y predicados relevantes y utilizar el método “Check-Sat” para verificar un modelo que satisfaga la consulta. Por ejemplo, si queremos encontrar una variable {unknown} que satisfaga la consulta, podemos escribir:
```
(declare-const unknown Language)
(assert (language unknown))
(check-sat)
(get-model)
```
Esto devolverá un modelo que asigna un valor a “unknown” que satisface la consulta. Si no se encuentra ningún modelo, significa que no hay variable que satisfaga la consulta.

Comments are closed.

es.davy.ai

¿Tienes una pregunta?

Tarea QnA para Z3. ¿Es posible?

Answer

davy.ai