Автоматическое доказательство теорем пролог

Пролог – декларативный язык, способный решать любые ребусы и доказывать теоремы

Время на прочтение
13 мин

Количество просмотров 52K

Представьте себе высокоуровневый язык, в котором не нужно указывать КАК получить результат, вместо этого нужно просто указать ЧТО вы хотите получить. При этом область применения языка не ограничена и язык способен решать те же задачи, что и любой другой высокоуровневый язык, наподобие JAVA. Кажется фантастикой, не правда ли? Однако такой язык есть и называется он PROLOG. Посмотрим как PROLOG справляется с этой задачей на примере загадывания прологу некоторых загадок и попросим PROLOG выдать доказательство теоремы.

Загадка 1. Простенькая, математическая. «?» — произвольная математическая операция (+,-,*,/), дано уравнение ((((1?2)?3)?4)?5)?6=35. Найти неизвестные операции.

Начнём описывать, что мы хотим получить. Поскольку знак операции неизвестен, он будет параметром.

formula(X1, X2, X3, X4, X5, X6, Sign1, Sign2, Sign3, Sign4, Sign5, Result):-
operation(X1, X2, Sign1, PartialResult1),
operation(PartialResult1, X3, Sign2, PartialResult2),
operation(PartialResult2, X4, Sign3, PartialResult3),
operation(PartialResult3, X5, Sign4, PartialResult4),
operation(PartialResult4, X6, Sign5, Result).

Эта строка описывает формулу 1?2?3?4?5?6=Result. Фактически, она означает: формула верна, если существуют частичный результат 1, частичный результат 2… частичный результат 4, такие что верны операции. Однако пролог не знает что такое операция, поэтому опишем в каких случаях они верны:

operation(X1, X2, «+», Result) :- Result = X1 + X2.
operation(X1, X2, «*», Result) :- Result = X1 * X2.
operation(X1, X2, «/», Result) :- Result = X1 / X2.
operation(X1, X2, «-«, Result) :- Result = X1 — X2.

Мы описали формулу, и теперь мы можем задавать любые вопросы относительно неё. Например, мы можем задать следующие вопросы: 1)если X1=1 X2=2 … X6=6 Result=35 то какие возможны операции? 2)указана часть числовых параметров и часть операций, а также результат, узнать, каковы недостающие параметры? 3)указаны все операции, числовые параметры, результат; узнать, верна ли формула. При этом не нужно заботиться о том, как именно пролог найдёт ответ – нужно просто задать вопрос.

Итак, вопрос:
askMainQuestion():-
formula(1,2,3,4,5,6,Sign1,Sign2,Sign3,Sign4,Sign5,35),
stdio::write(Sign1, Sign2, Sign3, Sign4, Sign5),
stdio::nl, %new line
fail.

Ответ: ++*++, +**+-, ***++ (Для задавания вопроса о числовых параметрах придётся написать ещё пару строк, но об этом чуть позже.)

Посмотреть код программы полностью (Visual Prolog 7.5)

implement main
open core

class predicates
askMainQuestion:() procedure.
operation: (real, real, string, real) multi(i,i,o,o).
formula: (real, real, real, real, real, real, string, string, string, string, string, real) nondeterm(i,i,i,i,i,i,o,o,o,o,o,i).
abs: (real, real) nondeterm (i,o).
clauses

operation(X1, X2, «+», Result) :- Result = X1 + X2.
operation(X1, X2, «-«, Result) :- Result = X1 — X2.
operation(X1, X2, «*», Result) :- Result = X1 * X2.
operation(X1, X2, «/», Result) :- Result = X1 / X2.

abs (X, Result) :- X>=0, Result=X.
abs (X, Result) :- X<0, Result=-X.

askMainQuestion():-
formula(1,2,3,4,5,6,Sign1,Sign2,Sign3,Sign4,Sign5,35),
stdio::write(Sign1, Sign2, Sign3, Sign4, Sign5),
stdio::nl,
fail.

askMainQuestion().

run() :-
console::init(),
askMainQuestion(),
_ = stdIO::readchar().

end implement main

goal
mainExe::run(main::run).

Загадка 2. Простенькая, нематематическая. Даны имена людей и родстенные отношения между ними. Найти всех братьев.

Укажем конкретные родственные связи:
parent(«Tom», «Jake»).
parent(«Jim», «Jake»).
parent(«Timmi», «Tom»).
uncle(«Tom»,«Peter»).
brother(«Timmi», «Cartman»).

Теперь опишем что означает родственная связь:

brother(Man1, Man2) :- parent(Man1, Parent), parent(Man2, Parent), Man1<>Man2.

(Человек1 и Человек2 братья, если существует ЧеловекРодитель, который является родителем для Человека1 и Человека2, и при этом Человек1 – это не Человек2).

brother(Man1, Man2) :- parent(ChildMan1, Man1), uncle(ChildMan1, Man2).

(Человек1 и Человек2 братья, если у Человека1 есть ребёнок, и Человек2 дядя этого ребёнка).

Теперь зададим вопрос о том, кто является братьями:

askMainQuestion():-
brother(X, Y),
stdIO::write(X, » «, Y),
stdio::nl,
fail.

Посмотреть код программы полностью

implement main
open core

class predicates
askMainQuestion:() procedure.
parent: (string, string) multi(o,o) nondeterm(o,i) nondeterm(i,o).
brother: (string, string) nondeterm(o,o) nondeterm(i,o).
uncle: (string, string) nondeterm anyflow.
clauses

parent(«Tom», «Jake»).
parent(«Jim», «Jake»).
parent(«Timmi», «Tom»).
uncle(«Tom»,«Peter»).

/*uncle(Man1, Man2) :- parent(Man1, ParentMan1), brother(ParentMan1, Man2). расскомментирование этой строки уронит программу*/
brother(«Timmi», «Cartman»).
brother(Man1, Man2) :- parent(ChildMan1, Man1), uncle(ChildMan1, Man2).
brother(Man1, Man2) :- parent(Man1, Parent), parent(Man2, Parent), Man1<>Man2.

askMainQuestion():-
brother(X, Y),
stdIO::write(X, » «, Y),
stdio::nl,
fail.

askMainQuestion().

run() :-
console::init(),
askMainQuestion(),
_ = stdIO::readchar().

end implement main
goal
mainExe::run(main::run).

Вывод программы: Timmi Cartman, Jake Peter, Tom Jim, Jim Tom. Сравните с тем, какое количество кода пришлось бы написать на императивном языке программирования.
Теперь давайте рассмотрим что-нибудь посложнее Hello World-ных программ и поговорим о подводных камнях пролога.

Загадка 3. На шахматной доске стоит 8 ферзей. Ни один ферзь не бьёт другого ферзя. Найти расположение ферзей.

Сначала опишем как может ходить ферзь:

attack(X1, Y1, X2, Y2) :- X2 = X1. %ферзь может атаковать, если атакуемая клетка и исходная на одной вертикали
attack(X1, Y1, X2, Y2) :- Y2 = Y1. % ферзь может атаковать, если атакуемая клетка и исходная на одной горизонтали
attack(X1, Y1, X2, Y2) :- abs(X2 — X1, Abs), abs(Y2 — Y1, Abs). %… на одной диагонали

Теперь укажем в каких случаях ферзь не может бить другого ферзя:

any(0).
any(1).
any(2).
any(3).
any(4).
any(5).
any(6).
any(7).
dontAttack(X1, Y1, X2, Y2) :-
any(X1), any(Y1), any(X2), any(Y2), not(attack(X1, Y1, X2, Y2)).

Тут возникает вопрос, зачем нужно перечисление всех возможных координат ферзя (any). Дело в том, что пролог устроен так, что он не может перебирать все возможные числовые или строковые значения. Все возможные значения величины, относительно которой задаётся вопрос, должны быть или перечислены в коде (как например, знаки в примере про нахождение знаков), или напрямую вычисляться на основе входных данных в вопросе (как например, результат формулы в примере про нахождение знаков, если в формуле не учитывать ошибки округления). Конечно, такое ограничение делает пролог не самым удобным языком для решения уравнений; однако, это никогда и не было основным предназначением этого языка.

Итак, мы описали, что означает что «один ферзь не бьёт другого ферзя», теперь нужно указать что каждый из 8 ферзей не бьёт другие 7 ферзей, однако писать 8*7=56 правил утомительно, поэтому опишем это правило рекурсивно. Зададим пустой массив и будем итеративно по одному добавлять в него по одному ферзю.

dontAttack([]).

(если нет ферзей, то никакой ферзь не бьёт никакого другого)

dontAttack(X, Y, []) :- any(X), any(Y).

(если есть один единственный ферзь, то он не бьёт других ферзей)

dontAttack(X1, Y1, [X2, Y2 | OtherElements]) :-
dontAttack([X2, Y2 | OtherElements]), dontAttack(X1, Y1, X2, Y2), dontAttack(X1, Y1, OtherElements).

(если есть ферзь с координатами X1 и Y1 и массив ферзей, то ни один ферзь не бьёт другого, если 1) внутри массива ферзей ни один ферзь не бьёт другого 2)ферзь (X1,Y1) не бьёт первого ферзя из массива ферзей 3)если убрать из массива ферзей первого ферзя, то в полученном множестве ферзей ни один ферзь также не бьёт другого )

dontAttack([X1, Y1 | OtherElements]) :-
dontAttack(X1, Y1, OtherElements).

(если есть ферзь с координатами X1 и Y1 и массив ферзей, и ни один ферзь не бьёт другого, то если добавить ферзя в массив ферзей, то ни один ферзь по-прежнему не будет бить другого)

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

askMainQuestion():-
X1=0, X2=1, X3=2, X4=3, X5=4, X6=5, X7=6, X8=7,
dontAttack ([X1, Y1, X2, Y2, X3, Y3, X4, Y4, X5, Y5, X6, Y6, X7, Y7, X8, Y8]),
stdio::write(X1, «:», Y1, » — «, X2, «:», Y2, » — «, X3, «:», Y3, » — «, X4, «:», Y4, » — «, X5, «:», Y5, » — «, X6, «:», Y6, » — «, X7, «:», Y7, » — «, X8, «:», Y8),
stdio::nl, %new line
fail.

Запускам программу и в ту же секунду получаем все возможные расстановки ферзей на шахматной доске.

Посмотреть код программы полностью

implement main
open core

class predicates
askMainQuestion:() procedure.
dontAttack: (integer, integer, integer, integer) nondeterm anyflow.
attack: (integer, integer, integer, integer) nondeterm(i,i,i,i). %nondeterm anyflow.
any:(integer) multi(o) determ(i).
dontAttack: (integer, integer, integer*) nondeterm anyflow.
dontAttack: (integer*) nondeterm anyflow.
abs: (integer, integer) nondeterm (i,o) nondeterm (i,i).
clauses

any(0).
any(1).
any(2).
any(3).
any(4).
any(5).
any(6).
any(7).

attack(X1, Y1, X2, Y2) :- X2 = X1.
attack(X1, Y1, X2, Y2) :- Y2 = Y1.
attack(X1, Y1, X2, Y2) :- abs(X2 — X1, Abs), abs(Y2 — Y1, Abs).

dontAttack(X1, Y1, X2, Y2) :-
any(X1), any(Y1), any(X2), any(Y2), not(attack(X1, Y1, X2, Y2)).

dontAttack(X1, Y1, [X2, Y2 | OtherElements]) :-
dontAttack([X2, Y2 | OtherElements]), dontAttack(X1, Y1, X2, Y2), dontAttack(X1, Y1, OtherElements).

dontAttack(X, Y, []) :- any(X), any(Y). %Граничное условие

dontAttack([X1, Y1 | OtherElements]) :-
dontAttack(X1, Y1, OtherElements).

dontAttack([]).

askMainQuestion().

abs(X, Result) :- X>=0, Result=X.
abs(X, Result) :- X<0, Result=-X.

run() :-
console::init(),
askMainQuestion(),
_ = stdIO::readchar().

end implement main

goal
mainExe::run(main::run).

Теперь давайте попросим пролог доказать простенькую теорему

Докажем, что подмножество группы является подгруппой тогда и только тогда, когда для любых элементов A и B из этого подмножества результат произведения A на обратный к B лежит в этом подмножестве. Для того, чтобы доказать, что подмножество является подгруппой, нужно доказать три пункта: 1)нейтральный элемент лежит в подмножестве 2)для каждого элемента из подмножества его обратный элемент лежит в подмножестве 3)произведение любых двух элементов подмножества лежит в подмножестве.

Обозначим нейтральный элемент как “E” и дадим определение нейтрального элемента:

operation(A, «E», A) :- any(A).
operation(«E», A, A) :- any(A).

Элемент нейтральный, если при умножении любого элемента на нейтральный получается исходный элемент. (например, в целых числах 1 – это нейтральный элемент).

Добавим парочку конкретных элементов.

any(«E»).
any(«M»).
any(«A»).
any(«B»).
any(«notA»).
any(«notB»).

Тут были введены некоторые другие элементы, помимо “E”, поясним что это за элементы, описав их свойства:

ofGroup(«M», «Set»).
ofGroup(«A», «SubSet»).
ofGroup(«B», «SubSet»).

А и B – элементы из подмножества, M – элемент из множества.

obratni(«B», «notB»).
obratni(«notB», «B»).
obratni(«A», «notA»).
obratni(«notA», «A»).
obratni(«E», «E»).

“notA” – обратный к “A”, “notB” – обратный к “B”

Теперь дадим определение обратного элемента:

operation(A, B, «E») :- obratni(A, B).
operation(B, A, «E») :- obratni(A, B).

А обратный к B, если при умножении A на B получается нейтральный элемент (например 2 * 0,5 = 1). Как видите, у A и B здесь нет кавычек, это значит что имеются ввиду не конкретные элементы «А» и «В», а любые элементы.

Определение подмножества:

ofGroup(X, «Set») :- ofGroup(X, «SubSet»).

(элемент принадлежит множеству, если он принадлежит подмножеству)

Теперь укажем, что для любых элементов A и B из подмножества результат произведения A на обратный к B лежит в этом подмножестве (по условию теоремы).

ofGroup(C, «SubSet») :- obratni(B, NotB), operation(A, NotB, C), ofGroup(A, «SubSet»), ofGroup(B, «SubSet»), stdio::write(C, » is from subset, because «, A, «*», NotB, «=», C, «. «), stdio::nl.

Как видите, здесь мы добавили вывод на экран (stdio::write), это сделано чтобы трассировать действия пролога, узнать как пролог использовал это правило, чтобы увидеть ход доказательства теоремы.

Теперь осталось доказать три пункта из теоремы.
Зададим вопрос про нейтральный элемент “E”:

firstQuestion() :-
ofGroup(«E», «SubSet»),
stdio::write(«E is from subset»),
!..
firstQuestion() :- stdio::write(«E is NOT from subset»).

Про обратный элемент:

secondQuestion():-
ofGroup(«notA», «SubSet»),
stdio::write(«notA is from subset»),
!..
secondQuestion() :- stdio::write(«NotA is NOT from subset»).

Тут у вас мог возникнуть вопрос: нужно доказать что для любого элемента из подмножества, его обратный элемент принадлежит подмножеству, однако в вопросе прологу мы указали один единственный конкретный элемент — «notA». На самом деле, поскольку мы не накладывали на элемент «notA» никаких ограничений (кроме того, что это обратный элемент к элементу, принадлежащего подмножеству), то если мы возьмём любой обратный элемент, то для него будут верны все те же рассуждения, которые мы применили к «notA». Математики часто пользуются этим приёмом при доказательстве теорем. Этот приём особенно важен для Prolog-а, ведь он не может перебирать все строковые и численные значения.

Ну и теперь зададим вопрос про принадлежность к подмножеству результата произведения двух элементов из подмножества:

operation(«A», «B», «AB»).
thirdQuestion():-
operation(«A», «B», AB),
ofGroup(AB, «SubSet»),
stdio::write(«A*B is from subset»),
!..
thirdQuestion() :- stdio::write(«A*B is NOT from subset»).

Запускаем… И программа падает, повиснув, от переполнения стека! Давайте разберёмся, почему это произошло. По сути, пролог пытается найти решение перебором введённых в него фактов. При поиске ответа на главный вопрос, пролог перебирает все факты, хоть как-то связанные с вопросом. Если неизвестно, истинен ли факт, он в свою очередь перебирает все факты, связанные уже с этим фактом. И так, пока не дойдёт до безусловных фактов, например до obratni(«A», «notA») – «notA» обратный к «A». Был задан вопрос: принадлежит ли нейтральный элемент к подмножеству. Пролог видит правило ofGroup(C, «SubSet») :- obratni(B, NotB), operation(A, NotB, C), ofGroup(A, «SubSet»), ofGroup(B, «SubSet») и понимает, что если в качестве С подставить нейтральный элемент и найти A и B, удовлетворяющие правилу, то согласно правилу нейтральный элемент будет принадлежать подмножеству. Первым элементом среди существующих указан как раз таки обратный ( any(«E») ), поэтому Prolog выбирает его в качестве B. Итак, obratni(«E», NotB). После этого Prolog задаёт вопрос: а какой элемент обратный к «E»? — и находит ответ ( obratni(«E», «E») ). Итак, NotB = «E». После этого Prolog идет дальше по правилу и видит operation(A, NotB, C), в данному случае operation(A, «E», «E») и задаёт вопрос: какой элемент при перемножении на «E» даёт «E» – и находит ответ «E» ( из правила operation(A, «E», «E») :- obratni(A, «E») и факта obratni(«E», «E»).). Итак, A = «E».Идём по исходному правилу дальше: ofGroup(A, «SubSet»), в данном случае ofGroup(«E», «SubSet»). И тут Prolog пытается ответить на тот же самый вопрос, что мы задавали вначале – а принадлежит ли «E» к «SubSet» (нейтральный к подгруппе)? Программа зацикливается и начинает снова перебирать те же самые факты и правила, ходя по замкнутому кругу. Ну что ж, перепишем немного исходное правило:

ofGroup(C, «SubSet») :- obratni(B, NotB), NotB<>«E», NotB<>«M», operation(A, NotB, C), ofGroup(A, «SubSet»), ofGroup(B, «SubSet»), stdio::write(C, » is from subset, because «, A, «*», NotB, «=», C, «. «), stdio::nl.

Теперь в качестве NotB нельзя использовать «E» и «M», и программа не повиснет (да-да, и на «M» она тоже повисает).
После этого программа в ту же секунду выдаёт доказательство трёх пунктов теоремы:

E is from subset, because B*notB=E.
E is from subset
(A и B лежат в подмножестве, поэтому произведение A на обратный к B лежит в подмножестве. В данном случае вместо A и B взят один и тот же элемент «B». Вывод доказательства можно сделать более подробным, если добавить больше команд write в правила)

E is from subset, because B*notB=E.
notA is from subset, because E*notA=notA.
notA is from subset

E is from subset, because B*notB=E.
notB is from subset, because E*notB=notB.
AB is from subset, because A*B=AB.
A*B is from subset

Посмотреть код программы полностью

implement main
open core

domains
any = string.
group = string.
class predicates
firstQuestion:() procedure.
secondQuestion:() procedure.
thirdQuestion:() procedure.
operation: (any, any, any) nondeterm(i,i,i) nondeterm(o,i,i) nondeterm(i,i,o) nondeterm(o,o,i) nondeterm(o,o,o) nondeterm(i,o,i) nondeterm(i,o,o) nondeterm(o,i,o).
obratni: (any, any) nondeterm(i,i) nondeterm(o,i) nondeterm(o,o) nondeterm(i,o).
ofGroup: (any, group) nondeterm(i,i) nondeterm(o,i) nondeterm(i,o).
any: (string) nondeterm(i) nondeterm(o).
clauses

operation(A, B, «E») :- obratni(A, B).
operation(B, A, «E») :- obratni(A, B).
operation(A, «E», A) :- any(A).
operation(«E», A, A) :- any(A). %коммутативность относительно нейтрального и обратного является следствием из ассоциативности, но не входит в миниммальное определение группы
operation(«A», «B», «AB»). %умножение А на В возможно

obratni(«M», «notM»).
obratni(«notM», «M»).
obratni(«B», «notB»).
obratni(«notB», «B»).
obratni(«A», «notA»).
obratni(«notA», «A»).
obratni(«E», «E»).

any(«E»).
any(«M»).
any(«A»).
any(«B»).
any(«notA»).
any(«notB»).
any(«notM»).

ofGroup(X, «Set») :- ofGroup(X, «SubSet»). %Определение подмножества
ofGroup(«E», «Set»).
ofGroup(«M», «Set»).
ofGroup(«A», «SubSet»).
ofGroup(«B», «SubSet»).
ofGroup(«notB», «Set»).
ofGroup(«notA», «Set»).

firstQuestion() :-
ofGroup(«E», «SubSet»),
stdio::write(«E is from subset»),
!..

firstQuestion() :- stdio::write(«E is NOT from subset»).

secondQuestion():-
ofGroup(«notA», «SubSet»),
stdio::write(«notA is from subset»),
!..

secondQuestion() :- stdio::write(«NotA is NOT from subset»).

thirdQuestion():-
operation(«A», «B», AB),
ofGroup(AB, «SubSet»),
stdio::write(«A*B is from subset»),
!..

thirdQuestion() :- stdio::write(«A*B is NOT from subset»).

run() :-
console::init(),
firstQuestion(),
stdio::nl,stdio::nl,stdio::nl,
secondQuestion(),
stdio::nl,stdio::nl,stdio::nl,
thirdQuestion(),
_ = stdIO::readchar().

end implement main

goal
mainExe::run(main::run).

Вывод

Prolog – замечательный декларативный язык, однако постоянные повисания не делают ему чести (если кто-нибудь знает способы борьбы с этим, просьба поделиться в комментариях). В самом деле, задача поиска циклов в графах решена давным давно, и устранение проблемы на уровне языка — вполне решаемая задача! Если бы эта проблема была решена, можно было бы составить базу знаний всех известных математических фактов, и задавать любые вопросы! Или например, изменить одну из базовых аксиом математики и в моментально узнать как изменятся другие законы (а-ля геометрия Лобачевского в мгновение ока)! Конечно, я настроен несколько оптимистично, и языку требуется немного больше доработок, но всё же… Например, одна из возможных доработок: Prolog должен уметь не только выходить из зацикливания, но и уметь обрабатывать зацикливания по определённым правилам, чтобы оперировать с бесконечными последовательностями, удовлетворяющими условию теоремы, как например в теореме Больцано-Вейерштрасса. Впрочем, в текущем состоянии Prolog врят ли пригоден вообще для чего бы то ни было: для поиска причин зацикливаний у меня ушло даже больше времени, чем для доказательства самой теоремы! (Имхо, всего лишь моё мнение)

Источник

��: ��

16.3.��

� �� , �� . �� �� �� , �� . �� �� , �� . �� , �� (� �� , �� ). �� , �� .

�� : �� , �� , �� , �.�. �� , �� . ��, ��, ��

p� v� ~ p

� ��»p��p«, �� , �� p.

�� :

~��, �� «��»

&��, �� «�»

v��, �� «��»

=>��, �� «��»

�� , �� «��» �� , �� «�», «��» � «��».

�� , �� , �� . �� , �� . �� , �� : �� , �� (�� ) �� (�.�. �� ). ��, �� , �� , �� .

�� . ��, �� , �� :

(� =>� b) & (b��=>� �) => (� =>� �)

�� : �� b�� b��,�� .

�� («�� »), �� . �� �� , ��

(�₁� v� p₂��v� �)� &� (q₁� v� q₂��v� �)

��&��(r₁� v� r₂� v� �)��&� �

���_i,�q_i,�r_i�� . �� , �� ��, �� (p₁�v p₂�v��)�� .

�� . � �� . � ��

(� =>� b)� &� (b� =>� �)� =>� (� =>��)

��

~((� =>� b) & (b� =>� �) => (� =>� �))

�� :

(1)�x�=>����~x�v��

(2)�~(x�v�y)�� ~x�&�~�

(3)�~(x�&��)��~x�v�~�

(4)�~(~x)��x

�� 1, ��

~(~((a �=>� b) �&� (b �=> ��)) �v� (� => ��))

��, �� 2 � 4 ��

(� =>� b)��&� (b� =>� �)� &� ~(ࠠ=>� �)

�� 1, ��

(~�� v� b)��&� (~b� v� �)� &� ~(~��v� �)

� ��, �� 2 ��

(~�� v� b)��&� (~b� v� �)� &� ��&� ~�

�� . �� .

�� , �� , � �� p, � � ��젗�~p.��

p�v�Y��蠠~p�v Z

�� :

Y� v� Z

�� , �� , �� . �� , �� (Y v�Z) � �� , �� . �� . �� «�� » (�� «nil») �� . ��, �� nil��

x��蠠~x

�� .

��.�16.6.�� (�=>b)&(b=>�)=>(a=>�) �� . �� ࠗ �� . �� , �� .

�� .�16.6 �� , �� .

�� .�16.7 �� , �� , �� . �� , �� . � �� :

��

�� C1��C2, ��P�� (��) ��C1,��~P��C2

��

�� P �� C1 (�� CA), �� ~P �� C2 (�� CB)�� CA�v�CB.

�� :

[ ��( C1), ��( P, C1, CA), ��( C2), ��( ~P, C2, CB) ] ---> �[ assert( ��( �� v ��) ) ].

�� . �� , �� , �� . �� .�16.7 ��

��( C1, C2, P)

� �� .

��, �� .�16.7, �� , � �� . �� , �� . �� . ��, ��

a� v� b� v� a

� �� a�v�b. �� , �� , ��,

a� v� b� v��~�

� �� , �� .

% �� % �� % �� [ ��( X), ��( ~X) ] ---> �[ write( '�� '), ��]. % �� [ ��( �), ��( P, �), ��( ~P, �) ] ---> �[ retract( �) ]. % �� [ ��( �), ��( P, �, C1), ��( P, C1) ] ---> �[ ��( ��( �), ��( C1) ) ]. % �� , �� [ ��( P), ��( �), ��( ~P, �, C1), � not ��( P, �, P) ] ---> �[ �ss�rt( ��( C1)), �ssert( ��( P, �, P))]. % �� , �� [ ��( ~P), ��( �), ��( P, �, C1), ��not ��( ~P, �, P) ] ---> �[ assert( ��( C1)), �ssert( ��( ~P, �, P))]. % �� , �� [ ��( C1), ��( P, C1, CA), ��( C2), ��( ~P, C2, CB), ��not ��( C1, C2, P) ] ---> �[ assert( ��(�CA v CB) ), ��assert( ��( C1, C2, P) ) ]. % �� : �� [] ---> [ write( '�� '), �� ]. % ��( P, E, E1) ��, �� E % �� E1, �� P ��( X, X v Y, Y). ��( X, Y v X, Y). ��( X, Y v Z, Y v Z1) :- ��( X, Z, Z1). ��( X, Y v Z, Y1 v Z) :- ��( X, Y, Y1). % ��( P, E) �� P �� % �� E ��( X, X). ��( X, Y) :- ��( X, Y, _ ).

��.�16.7.��, �� , �� .

�� : �� ? �� , �� .�16.8. ��

��( ��)

�� C1,�C2�� .�. � �� assert � ��

��( C1). ��( C2). ...

��, �� , �� ��. �� , �� , �� , � �� . � �� :

?-��(~(( �=>b) & ( b=>c) => ( �=>�))�),��.

�� «�� » �� , �� .

% �� % �� assert :- op( 100, fy, ~).��% �� :- op( 110, xfy, &).��% �� :- op( 120, xfy, v).��% �� :- op( 130, xfy, =>).��% �� ( F & G) :-�!,��% �� ( F), ��( G). ��( ��) :- ��( ��, ��),�!,�% �� ( ��). ��( ��) :-��% �� assert( ��( ��) ). % �� ( ~( ~X), X) :-�!.��% �� ( X => Y, ~X v Y) :-�!.��% �� ( ~( X & Y), ~X v ~Y) :-�!. % �� ( ~( X v Y), ~X & ~Y) :-�!. % �� ( X & Y v Z, (X v Z) & (Y v Z) ) :-�!. ��% �� ( X v Y & Z, (X v Y) & (X v Z) ) :-�!. ��% �� ( X v Y, X1 v Y) :-��% �� ( X, X1),�!. ��( X v Y, X v Y1) :-��% �� ( Y, Y1),�!. ��( ~X, ~�1) :-��% �� ( X, X1).

��.�16.8.�� assert.

Источник

DOMAINS
  EXPR=con(EXPR,EXPR);  % конъюнкция
  impl(EXPR,EXPR);      % импликация
  no(EXPR);             % отрицание
  var(symbol).          % переменная
PREDICATES
  nondeterm reduce(EXPR,EXPR,integer)
CLAUSES
% терминальное тождество: p -> p, где p - переменная
  reduce(var(X),var(X),_):- nl, write("Тождество: "), write("var("),
  write(X), write(") => var("), write(X), write(")").
 
% терминальное тождество: ^p -> ^p, где p - переменная
  reduce(no(var(X)),no(var(X)),_):- nl, write("Тождество: "), write("no(var("),
  write(X), write(")) => no(var("), write(X), write("))").
 
% p & (q & r) -> (p & q) & r
  reduce(con(P,con(Q,R)),con(con(P1,Q1),R1),N) :- nl,write("Правило 2: "),  
  write("con("), write(P), write(",con("), write(Q),write(","), write(R),  
  write(")) => con(con("), write(P), write(","),write(Q), write("),"), write(R), 
  write(")"),reduce(P,P1,0), reduce(Q,Q1,0), reduce(R,R1,0).
 
% p & (p > q) -> q
  reduce(con(P,impl(P,Q)),Q1,N):- reduce(Q,Q1,0),
  nl, write("Правило 3: "), write("con("), write(P), write(",impl("),
  write(P), write(","), write(Q1), write(")) => "), write(Q1).
 
% ^q & (p > q) -> ^p
reduce(con(no(Q),impl(P,Q)),no(P1),N):- reduce(P,P1,0),nl, 
write("Правило 4: "), write("con(no("), write(Q), 
write("),impl("),write(P1), write(","), write(Q), write(")) => "), 
write("no("), write(P1), write(")").
 
% q & (p > ^q) -> ^p
  reduce(con(Q1,impl(P,no(Q1))),no(P1),N):- reduce(P,P1,N),
  reduce(Q1,no(no(Q1)),0), nl, write("Правило 4.1: "), write("con(no(no("),  
  write(Q1), write(")),impl("), write(P1), write(",no("), write(Q1), 
  write("))) => "), write("no("), write(P1),write(")").
 
% ^^p -> p
  reduce(no(no(P)),P1,N):- reduce(P,P1,0), nl, write("Правило 5: "), 
  write("no(no("), write(P1),write(")) => "),  write(P1).
 
% ^P->^P' (P->P')
  reduce(no(P),no(P1),N):- reduce(P,P1,0),  nl, write("           "), 
  write("no("), write(P),write(") => no("),  write(P1), write(")").
 
% p & q -> q & p
  reduce(con(P,Q),X,0):- nl, write("Правило 1: "), write("con("), write(P), 
  write(","), write(Q), write(") => "), write("con("), write(Q), write(","), 
  write(P), write(")"), reduce(con(Q,P),X,1).
 
  reduce(con(P,Q),X,0):- reduce(P,P1,1),reduce(Q,Q1,1), reduce(con(P1,Q1),X,1),
  nl, write("           "), write("con("), write(P1), write(","), write(Q1),
  write(") => "), write("con("), write(Q1), write(","), write(P1).
 
% p -> ^^p
  reduce(X1,no(no(X)),K):- K<2, reduce(X1,X,2),nl, write("Правило 6: "), 
  write(X), write(" => "), write("no(no("), write(X),write("))").
 
% терминальное тождество: p -> p
  reduce(X, X, _):- nl, write("           "), write(X), write(" => "), write(X).
 
GOAL
  K= con( impl( var(t), no(var(s)) ), var(t) ),
  nl,write("Выражение:"),nl, write(K),nl, write("Вывод:"), nl, reduce(K,X,0), 
  nl, write("Ответ:"),nl, write(X),write("."),nl.

Источник

Автоматическое доказательство теорем

Страницы работы

Фрагмент текста работы

МО РФ

НГТУ

Кафедра
прикладной математики и информатики

Лабораторная работа №6

“Автоматическое доказательство теорем“

по предмету:
Системы искусственного интеллекта

Факультет: ПМи

Группа: ПМ-93

Студенты: Исаева А.В., Щербакова Н.В., Шишкин Р.Н.

Преподаватель: Целебровская М.Ю.

Новосибирск
2003

Цель
работы

Изучение машинных методов доказательства теорем для
простых формальных систем

Задание

§ Рассмотреть заданную формальную систему и
сформулированную в рамках данной системы теорему. Доказать эту теорему
«вручную».

§ Написать программу автоматического доказательства
теорем на Прологе, используя основные свойства среды Пролога – поиск с
возвратом и унификацию.

§ Использовать метод Сиклосси-Маринова (реализовать
соответствующую эвристику) для ограничения пространства поиска доказательства.

§ Ввести в программу возможность вывода хода
доказательства.

Рассматриваются
следующие шесть правил вывода:

Требуется
доказать теорему:

Доказательство: .

Анализ
задачи

Для обеспечения нормальной работы
программы доказательства теорем необходимо произвести переупорядочивание
заданных правил. Это связано с тем, что некоторые правила преобразуют выражение
так, что к результату может быть применимо то же самое правило (такие правила
называются экстенсивными), и использование таких правил порождает бесконечное
множество формул, поэтому их применение должно быть как-то ограничено. Также
некоторые из правил составляют группу взаимообратных, что тоже может привести к
бесконечной процедуре поиска, поэтому в предикатах вводится дополнительное
ограничение на последовательность применения таких правил. Ниже приведены переупорядоченные
правила

Сиклосии и Маринов предложили
рассматривать экстенсивные правила только тогда, когда обойтись без них
невозможно и в таком случае эти правила применяются не более одного раза для
уровня текущего поиска, а полный поиск по всем другим правилам отсекается.

Тестовые
примеры

Выражение: con(impl(var(«s»),no(var(«t»))),var(«t»))

Доказательство:

Правило 1:
con(impl(var(«s»),no(var(«t»))),var(«t»)) =>

con(var(«t»),impl(var(«s»),no(var(«t»))))

Тождество: var(s) => var(s)

Тождество: var(t) => var(t)

Правило 6: var(«t») => no(no(var(«t»)))

Правило 4.1:
con(no(no(var(«t»))),impl(var(«s»),no(var(«t»))))
=> no(var(«s»))

Ответ: no(var(«s»)).

Выражение: con(con(var(«a»),var(«b»)),impl(con(var(«a»),var(«b»)),var(«q»)))

Доказательство:

Тождество: var(q) => var(q)

Правило 3:
con(con(var(«a»),var(«b»)),impl(con(var(«a»),var(«b»)),var(«q»)))
=> var(«q»)

Ответ: var(«q»).

Выражение:

con(impl(var(«t»),con(impl(con(var(«a»),var(«b»)),var(«q»)),con(var(«a»),var(«b»)))),var(«t»))

Доказательство:

Правило 1:

con(impl(var(«t»),con(impl(con(var(«a»),var(«b»)),var(«q»)),con(var(«a»),var(«b»)))),var(«t»))
=>
con(var(«t»),impl(var(«t»),con(impl(con(var(«a»),var(«b»)),var(«q»)),con(var(«a»),var(«b»)))))

Правило 1: con(impl(con(var(«a»),var(«b»)),var(«q»)),con(var(«a»),var(«b»)))
=>

con(con(var(«a»),var(«b»)),impl(con(var(«a»),var(«b»)),var(«q»)))

Тождество: var(q) => var(q)

Правило 3:
con(con(var(«a»),var(«b»)),impl(con(var(«a»),var(«b»)),var(«q»)))
=> var(«q»)

Правило 3: con(var(«t»),impl(var(«t»),var(«q»)))
=> var(«q»)

Ответ: var(«q»).

Выражение: con(var(«a»),var(«b»))

Доказательство:

Правило 1: con(var(«a»),var(«b»)) =>
con(var(«b»),var(«a»))

Тождество: var(a) => var(a)

Тождество: var(b) => var(b)

con(var(«a»),var(«b»)) =>
con(var(«a»),var(«b»))

Правило 6: con(var(«a»),var(«b»)) =>
no(no(con(var(«a»),var(«b»))))

con(var(«a»),var(«b»)) =>
con(var(«b»),var(«a»)

Ответ: no(no(con(var(«a»),var(«b»)))).

Выражение: con(no(con(var(«p»),impl(var(«p»),var(«q»)))),impl(var(«p»),var(«q»)))

Доказательство:

Правило 1:

con(no(con(var(«p»),impl(var(«p»),var(«q»)))),impl(var(«p»),var(«q»)))
=> con(impl(var(«p»),var(«q»)),no(con(var(«p»),impl(var(«p»),var(«q»)))))

Тождество: var(q) => var(q)

Правило 3:
con(var(«p»),impl(var(«p»),var(«q»))) =>
var(«q»)

no(con(var(«p»),impl(var(«p»),var(«q»))))
=> no(var(«q»))

impl(var(«p»),var(«q»)) =>
impl(var(«p»),var(«q»))

Правило 6: impl(var(«p»),var(«q»)) =>
no(no(impl(var(«p»),var(«q»))))

impl(var(«p»),var(«q»)) =>
impl(var(«p»),var(«q»))

Тождество: var(p) => var(p)

Правило 4:
con(no(var(«q»)),impl(var(«p»),var(«q»))) =>
no(var(«p»))

Правило 1:

con(no(var(«q»)),impl(var(«p»),var(«q»)))
=> con(impl(var(«p»),var(«q»)),no(var(«q»))

Ответ:
no(var(«p»)).

Текст программы

DOMAINS

EXPR=con(EXPR,EXPR); % конъюнкция

impl(EXPR,EXPR); % импликация

no(EXPR); % отрицание

var(symbol). % переменная

PREDICATES

nondeterm reduce(EXPR,EXPR,integer)

CLAUSES

% терминальное тождество: p -> p, где p — переменная

reduce(var(X),var(X),_):- nl,
write(«Тождество: «),
write(«var(«),

write(X), write(«) => var(«),
write(X), write(«)»).

% терминальное тождество: ^p -> ^p, где p — переменная

reduce(no(var(X)),no(var(X)),_):- nl,
write(«Тождество: «),
write(«no(var(«),

write(X), write(«)) =>
no(var(«), write(X), write(«))»).

% p & (q & r) -> (p & q)
& r

reduce(con(P,con(Q,R)),con(con(P1,Q1),R1),N)
:- nl,write(«Правило 2: «),

write(«con(«), write(P),
write(«,con(«), write(Q),write(«,»), write(R),

write(«)) => con(con(«),
write(P), write(«,»),write(Q), write(«),»), write(R),

write(«)»),reduce(P,P1,0), reduce(Q,Q1,0),
reduce(R,R1,0).

% p & (p > q) -> q

reduce(con(P,impl(P,Q)),Q1,N):-
reduce(Q,Q1,0),

nl, write(«Правило 3: «), write(«con(«), write(P),
write(«,impl(«),

write(P), write(«,»),
write(Q1), write(«)) => «), write(Q1).

% ^q & (p > q) -> ^p

reduce(con(no(Q),impl(P,Q)),no(P1),N):-
reduce(P,P1,0),nl, write(«Правило 4: «),
write(«con(no(«), write(Q), write(«),impl(«),write(P1),
write(«,»), write(Q), write(«)) => «),
write(«no(«), write(P1), write(«)»).

% q & (p > ^q) -> ^p

reduce(con(Q1,impl(P,no(Q1))),no(P1),N):-
reduce(P,P1,N),

reduce(Q1,no(no(Q1)),0), nl,
write(«Правило 4.1: «),
write(«con(no(no(«),

write(Q1),
write(«)),impl(«), write(P1), write(«,no(«), write(Q1),

write(«))) => «),
write(«no(«), write(P1),write(«)»).

% ^^p -> p

reduce(no(no(P)),P1,N):-
reduce(P,P1,0), nl, write(«Правило 5: «),

write(«no(no(«),
write(P1),write(«)) => «), write(P1).

% ^P->^P’ (P->P’)

reduce(no(P),no(P1),N):-
reduce(P,P1,0), nl, write(» «),

write(«no(«),
write(P),write(«) => no(«), write(P1), write(«)»).

% p & q -> q & p

reduce(con(P,Q),X,0):- nl,
write(«Правило

Информация о работе

Источник

Читайте также

Программы для автоматического заполнения форм

Программы для автоматического заполнения форм
Во время интернет-серфинга часто приходится заполнять различные формы на веб-страницах, указывая при этом одни и те же данные: фамилию, имя, адрес, дату рождения и многое другое. С помощью специальных программ можно сохранить

7.4.3. Kudzu — утилита для автоматического определения устройств

7.4.3. Kudzu — утилита для автоматического определения устройств
В Linux для автоматического определения устройств используется специальная утилита kudzu, названная в честь китайской лианы — злостного сорняка. В дистрибутивы, основанные на Linux Mandrake, вместо нее может входить

Глава 2 Roger Wilco — самая простая программа голосового общения

Глава 2
Roger Wilco — самая простая программа голосового

Глава 3 Простая на первый взгляд программа TeamTalk

Глава 3
Простая на первый взгляд программа TeamTalk

Программы для автоматического заполнения форм

Программы для автоматического заполнения форм
Программы для автоматического заполнения форм состоят из двух главных частей. Это базы данных, где сохраняются сведения, используемые при вводе различных форм, и собственно средства ввода. Удобство использования таких

Глава 11 Создание меню автоматического определения компакт-дисков

Глава 11
Создание меню автоматического определения компакт-дисков
• Автозапуск.• Интерфейс программы AutoPlay Menu Builder.• Элементы управления.• Присвоение команд элементам меню.• Практические

8.3. Программа автоматического переключения раскладки клавиатуры Punto Switcher

8.3. Программа автоматического переключения раскладки клавиатуры Punto Switcher
Еще одним средством, которое поможет значительно ускорить набор, являются программы автоматического переключения клавиатурных раскладок. Если в вашем тексте встречаются и русские, и английские

Глава 14 PSPICE и техника автоматического регулирования

Глава 14
PSPICE и техника автоматического регулирования

Эта глава откроет перед вами окно в мир фантастических возможностей, которые предоставляет программа PSPICE при моделировании регулируемых цепей.
PSPICE обладает непревзойденной гибкостью при конструировании сложнейших

Пример: простая программа с уведомлением

Пример: простая программа с уведомлением
Прежде чем углубляться в тонкости сигналов реального времени и потоков Posix, мы напишем простейшую программу, включающую отправку сигнала SI6USR1 при помещении сообщения в пустую очередь. Эта программа приведена в листинге 5.8, и мы

Доказательства теорем

Доказательства теорем
Компьютер можно использовать для доказательства теорем. Это — трудная задача искусственного интеллекта. Мы снабжаем компьютер правилами вывода, даем формулировку того, что требуется доказать, и исходные аксиомы. Компьютер пытается найти

Осторожность в отношении автоматического преобразования типов

Осторожность в отношении автоматического преобразования типов
Часто мы используем совместно символы и строки, не обращая на это никакого внимания. Преобразованием типов занимается компилятор, и программист зачастую не подозревает, что происходит на самом деле.

Инструмент автоматического создания фоновой музыки

Инструмент автоматического создания фоновой музыки
Очень полезной является возможность автоматического создания фоновой музыки в заданном стиле произвольной длительности. Для этого используют инструмент Фоновая музыка аудиоинструментария, окно которого показано на

Стандартный способ автоматического запуска программ

Стандартный способ автоматического запуска программ
Ветвь HKEY_CURRENT_USERSoftwareMicrosoftWindows NTCurrentVersionWindows также может содержать параметры, значения которых будут загружаться при входе пользователя в систему. Рассмотрим их (все они имеют строковый тип).• Load – определяет программы

7.3. Программы автоматического переключения раскладки клавиатуры (Punto Switcher)

7.3. Программы автоматического переключения раскладки клавиатуры (Punto Switcher)
Еще одним средством, которое поможет значительно ускорить набор, являются программы автоматического переключения клавиатурных раскладок. Если в вашем тексте встречаются и русские, и английские

Ингредиенты доказательства корректности цикла

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

Источник

I was reluctant to post an Answer because this Question is poorly framed. Thanks to theJollySin for adding clean formatting! Something omitted in the rewrite, indicative of what Aman had in mind, was «I inter in Loop» (sic).

We don’t know what query was entered that resulted in this looping, so speculation is required. The two rules suggest that Goal involved either the parallel/2 or the perpendicular/2 predicate.

With practice it’s not hard to understand what the Prolog engine will do when a query is posed, especially a single goal query. Prolog uses a pretty simple «follow your nose» strategy in attempting to satisfy a goal. Look for the rules for whichever predicate is invoked. Then see if any of those rules, starting with the first and going down in the list of them, can be applied.

There are three topics that beginning Prolog programmers will typically struggle with. One is the recursive nature of the search the Prolog engine makes. Here the only rule for parallel/2 has a right-hand side that invokes two subgoals for perpendicular/2, while the only rule for perpendicular/2 invokes both a subgoal for itself and another subgoal for parallel/2. One should expect that trying to satisfy either kind of query inevitably leads to a Hydra-like struggle with bifurcating heads.

The second topic we see in this example is the use of free variables. If we are to gain knowledge about perpendicularity or parallelism of two specific lines (geometry), then somehow the query or the rules need to provide «binding» of variables to «ground» terms. Again without the actual Goal being queried, it’s hard to guess how Aman expected that to work. Perhaps there should have been «facts» supplied about specific lines that are perpendicular or parallel. Lines could be represented merely as atoms (perhaps lowercase letters), but Prolog variables are names that begin with an uppercase letter (as in the two given rules) or with an underscore (_) character.

Finally the third topic that can be quite confusing is how Prolog handles negation. There’s only a touch of that in these rules, the place where X==Y is invoked. But even that brief subgoal requires careful understanding. Prolog implements «negation as failure», so that X==Y succeeds if and only if X==Y does not succeed. This latter goal is also subtle, because it asks whether X and Y are the same without trying to do any unification. Thus if these are different variables, both free, then X==Y fails (and X==Ysucceeds). On the other hand, the only way for X==Yto succeed (and thus for X==Y to fail) would be if both variables were bound to the same ground term. As discussed above the two rules as stated don’t provide a way for that to be the case, though something might have taken care of this in the query Goal.

The homework assignment for Aman is to learn about these Prolog topics:

recursion
free and bound variables
negation

Perhaps more concrete suggestions can then be made about Prolog doing geometry proofs!

Added: PTTP (Prolog Technology Theorem Prover) was written by M.E. Stickel in the late 1980’s, and this 2006 web page describes it and links to a download.

It also summarizes succinctly why Prolog alone is not » a full general-purpose theorem-proving system.» Pointers to later, more capable theorem provers can be followed there as well.

Источник

I’m looking for an automatic theorem proving system, which can prove this:

Crocodile took mans child. Man asked crocodile not to eat his child. But Crocodile said: I’ll return your child to you, if you will tell me, what am I going to do with him.

Analytical solution to his looks like this:

x — crocodile will eat child
y — men answers: crocodile will eat child

~ means equality, ! means not, -> implies, + OR;

((x~y)->!x) and  ((x XOR y)->x) =
(x! and y +!x and y+!x)(!x!y+x and y+x) =
(!x+!y)(x+!y) = !y;

So, the answers is that men has to say: «You are not going to eat the child»;

Now, there are plenty of systems listed here:
http://en.wikipedia.org/wiki/Automated_theorem_proving

I’ve tried 5-6 of them, but couldn’t really understand what am I doing here. How to formalize this theorem inside them, so that I could enter this first part of it:

((x~y)->!x) and ((x XOR y)->x)

and get the answer

y as an output.

Can any once advice, which system at least capable of doing so automatically, and give me some more hints?

Regards,
Konstantin.

Источник

Пролог – декларативный язык, способный решать любые ребусы и доказывать теоремы

Загадка 1. Простенькая, математическая. «?» — произвольная математическая операция (+,-,*,/), дано уравнение ((((1?2)?3)?4)?5)?6=35. Найти неизвестные операции.

Загадка 2. Простенькая, нематематическая. Даны имена людей и родстенные отношения между ними. Найти всех братьев.

Загадка 3. На шахматной доске стоит 8 ферзей. Ни один ферзь не бьёт другого ферзя. Найти расположение ферзей.

Теперь давайте попросим пролог доказать простенькую теорему

Вывод

�����: ���������������� �� ����� ������ ��� �������������� ����������

Автоматическое доказательство теорем

Страницы работы

Фрагмент текста работы

МО РФ

НГТУ

Кафедра прикладной математики и информатики

по предмету: Системы искусственного интеллекта

Факультет: ПМи

Группа: ПМ-93

Студенты: Исаева А.В., Щербакова Н.В., Шишкин Р.Н.

Преподаватель: Целебровская М.Ю.

Новосибирск 2003

Цель работы

Задание

Анализ задачи

Тестовые примеры

Текст программы

Информация о работе

Читайте также

Программы для автоматического заполнения форм

7.4.3. Kudzu — утилита для автоматического определения устройств

Глава 2 Roger Wilco — самая простая программа голосового общения

Глава 3 Простая на первый взгляд программа TeamTalk

Программы для автоматического заполнения форм

Глава 11 Создание меню автоматического определения компакт-дисков

8.3. Программа автоматического переключения раскладки клавиатуры Punto Switcher

Глава 14 PSPICE и техника автоматического регулирования

Пример: простая программа с уведомлением

Доказательства теорем

Осторожность в отношении автоматического преобразования типов

Инструмент автоматического создания фоновой музыки

Стандартный способ автоматического запуска программ

7.3. Программы автоматического переключения раскладки клавиатуры (Punto Switcher)

Ингредиенты доказательства корректности цикла

Добавить комментарий Отменить ответ

��: ��

Кафедра
прикладной математики и информатики

по предмету:
Системы искусственного интеллекта

Новосибирск
2003

Цель
работы

Анализ
задачи

Тестовые
примеры