Как решить единицу разрешения? - PullRequest
1 голос
/ 07 июня 2011

Как я могу выразить разрешение в единицах кода? Например:

A1
-(A1 & A2 & A3 ... & An)

где - Нет, а & является оператором и .

Ответ должен быть:

-(A2 & ... & An)

Как бы я написал это, например, на прологе (или на языке scala, или на каком-нибудь другом)?

По-моему, это должна быть какая-то функция, которая делает что-то вроде этого:

def unitResolution(sentence1, sentence2, ... sentence_n) : result

Любая помощь приветствуется.

Ответы [ 2 ]

2 голосов
/ 11 июня 2011

Идея состоит в том, чтобы использовать блочную директиву Prolog для запуска разрешения единиц измерения. Об этой технике есть очень хорошая статья Howe & King "Жемчужина по SAT и SMT-решению в Прологе", а также исходный код: http://www.soi.city.ac.uk/~jacob/solver/. Мы используем аналогичную технику в решении проблем нашего инструмента ProB, написанного на Прологе (если вы действительно заинтересованы, вы можете найти недавнюю статью здесь: http://www.stups.uni -duesseldorf.de / publishing_detail.php? Id = 325 ).

2 голосов
/ 07 июня 2011

Подобная проблема недавно произошла со мной. Я изложил это немного по-другому. Предположим, у нас есть программа Prolog. И вместо того, чтобы делать обратное пение (которое является входным разрешением) мы хотели бы сделать прямую цепочку (которая является единичным разрешением).

Я еще не полностью реализовал это. Но можно попробовать следующее. Нормальный Правило обратной цепочки выглядит следующим образом:

p :- q1, q2, q3, .., qn. /* backward */

Теперь правило прямой цепочки, которое разрешает юниты с первой целью, просто переключает положение р и q1. Таким образом это выглядело бы следующим образом:

q1 :- p, q2, .., qn. /* forward */

Затем можно воспользоваться индексацией предикатов Prolog для поиска предложения соответствия в шаг разрешения. Давайте посмотрим на шаг разрешения с единицей r первым в случай нормального правила обратной цепочки. Предположим, что единица r объединяется с q1. Итак новый пункт будет:

p' :- q2', q3', ..., qn'. /* backward */

Апостроф указывает, что МГУ был применен. Теперь мы хотим, чтобы наш алгоритм привести новые правила в прямом обозначении. Это будет:

q2' :- p',  q3', ..., qn'. /* forward */

Или в Прологе, предполагая, что оператор (,) / 2 равен xfy:

% resolution_step(+Unit,+TrickyClause,-TrickyClause or Unit)  
resolution_step(U,(U :- H, G, B),(G :- H, B)).  
resolution_step(U,(U :- H, G),(G :- H)).  
resolution_step(U,(U :- H),H).  

Здесь вы видите, как это можно использовать итеративно. Я использую предикатную повестку дня / 1, чтобы держать единицы. И база данных Пролога для хранения хитрых предложений, а также недавно созданных. Таким образом, предикаты, которые вступают в игру, должны быть объявлены динамическими.

iterate :-  
  agenda(U),  
  clause(U,B),  
  resolution_step(U,(U:-B),C),  
  (C=(P :- Q) -> assertz((P:-Q)); assertz(agenda(C))).

Теперь нужно выполнять итерации, пока есть изменения, и избегать создания дубликатов. Или избегайте вариантов или подсчетов. Если в сложных пунктах больше нет дельты или если в повестке дня нет больше дельты, мы можем остановиться на нашем поиске вперед. Конечно, мы могли бы также остановиться на поиске вперед, если найдена определенная цель.

Но теперь вы видите проблему с этим шагом разрешения одного устройства. Промежуточными результатами являются не только новые единицы, но и новые неединичные предложения. Таким образом, на практике, я полагаю, не нужно реализовывать шаг разрешения с единичным разрешением, а то, что стало известно как гиперразрешение. А именно, разрешение предложения с несколькими единицами, чтобы создать новый модуль.

Гиперразрешение упростило бы управление итерацией. Нет необходимости хранить промежуточные неединичные предложения, и дельта может быть легче обнаружена. Также новые дельты могут быть вычислены на основе предыдущих дельт. Избегать излишней переоценки форвардных правил. Но в гиперразрешении мы теряем преимущество индексации наших хитрых предложений. Так что я все еще жду интересного предложения о представлении Прологом гиперслоя в подходящем представлении форвардных предложений.

С наилучшими пожеланиями

Изменить 10.04.2012:
Тем временем я нашел способ сделать гиперразрешение. Он основан на преобразовании предложения:

P :- A

В пункт:

delta(X,P) :- A_new(X)

посредством расширения пункта. Дельта должна вычислить в P результат разрешения для того, когда прибыл новый блок X. Я уже сделал пару успешных экспериментов (*) (* *), но индексация еще не была реализована. У меня есть концепция индексации, основанная на перемещении определенных условий на X в начало правила, но я еще не успел ее реализовать.

(*) 8 королев через разрешение блока
https://plus.google.com/u/0/b/103259555581227445618/103259555581227445618/posts/2q6nd6VbgZJ

(* *) Парсер диаграммы Earley через разрешение устройства
https://plus.google.com/u/0/b/103259555581227445618/103259555581227445618/posts/4tFbxLbknYe

...