Доброго времени, дорогие Кодфорсчане!
Я хочу разрекламировать результат своей бакалаврской жизнедеятельности, программу MathLogic. Её можно бесплатно (в прошлом планируется взимание таксы) скачать с сайта, посвящённого мне: http://balancedtree.lv. Акция проходит в рамках осенней распродажи купонов на бесплатные программные обеспечения и сухари.
Прошу судить мягко и выражаться о программе здесь.
UPD: добавил ссылку на mercurial repository этой программы на сайт -- http://logic:[email protected]/scm/hg/logic.
Welcome to my web site! Your external IP, browser address, and visit date/time are saved in server logs for analytics.
(1) ⊢(p∧q)→p is Axiom
(2) ⊢((a∧b)∧c)→(a∧b) by Substitution of (1) with {p↦a∧b,q↦c}
(3) ⊢p→(p∨q) is Axiom
(4) ⊢(((a∧b)∧c)→(a∧b))→((((a∧b)∧c)→(a∧b))∨¬(b∧c)) by Substitution of (3) with {p↦((a∧b)∧c)→(a∧b),q↦¬(b∧c)}
(5) ⊢(((a∧b)∧c)→(a∧b))∨¬(b∧c) by Detachment of Premises (2) and (4)
Кажется под конец коммента начал доходить смысл вашей работы: с одной стороны, можно побрутфорсить abc значениями 000..111, вычисляя с использованием польской нотации результат, в случае тождественности 0 всего выражения можно будет вывести дерево вычислений, это будет довольно информативно (типа контрпример, почему теорему доказать нельзя). С другой стороны, если выражение истинно при всех наборах — то это нифига не информативно, хотя в этом случае теорема верна. Можно тогда дать его этой программе, а она докажет, почему же выражение всегда 1. Я бы на вашем месте начал как раз с брутфорса, странно что вы решили наоборот))
Но для меня проблема "как этим пользоваться" остается проблемой. Пока что я даже не знаю, как через нее доказать, что "у каждого человека есть мать".
Konstantin.Zakharov, спасибо! Над кодировкой думаю. Кажется, это из-за моего копирования между Win/Linux системами лажа случилась. Maven отпадает, я его не люблю :(.
В случае, если утверждение не истинно, то программа не строит доказательство обратного утверждения автоматически. Это можно сделать вручную, добавив отрицание перед высказыванием.
Перебор (brute force) я делал в разных вариациях, в итоге через него определяется, стоит ли вообще доказывать теорему (верна ли она).
То, что у каждого человека есть мать, через неё доказать нельзя -- она не поддерживает кванторы.
Перебор (brute force) я делал в разных вариациях, в итоге через него определяется, стоит ли вообще доказывать теорему (верна ли она).
Значит зря вы так слили свой перебор, вывод строки "Theorem cannot be proven" это не предел его способностей, как я и сказал выше. Как говорят в фейсбуке — concentrate on impact, т.е. делай то, что вызовет наибольший эффект. А вы писали несколько вариаций перебора, чтобы воткнуть его под if( solvable() ) solve() ? Можно даже так — взять все наборы, на которых выражение ложно, потом каким-то эвристическим ̶г̶о̶в̶н̶о̶к̶о̶д̶о̶м̶ алгоритмом, анализирующим вид выражения, выделить наиболее показательные (типа, "батенька, да у вас же тут все на 0 умножилось"), а потом сделать об этом публикацию в научный журнал, который никто не читает (зато прикольно).
То, что у каждого человека есть мать, через неё доказать нельзя -- она не поддерживает кванторы.
Тогда стоило во вкладку Theorem при запуске рандомно закидывать один из 10 примеров только на высказываниях, демонстрирующих как блистательно ваша программа может разруливать бытовые непонятки/взрывать бюрократические гадюшники/унижать в прямом эфире.
Честно говоря, программа в общем-то основана на переборе, просто в неявном виде, поэтому я в предыдущем комментарии Вам наврал.
Но я так понимаю, по Вашей интонации, что надо куда-то в более влиятельные журналы было бы публиковаться, на понятных обществу языках, так сказать (английский, хинди)?
Про "батенька, да у вас же тут все на 0 умножилось" мне товарищ начальник учебной программы Арницанс предлагал, я отказался по причине уклонения от цели работы.
Помнится я на втором или третьем курсе такую программку писал, чтобы практики по мат логике решать.
У нас на втором написать брутфорс было обязательное задание (строго говоря, надо было выводить СКНФ/СДНФ).
Круто, а у Вас не осталось каких-нибудь остатков тех былых программ?
Я таких сайтов лет 10 уже не видел — он просто шедеврален! Начиная от названия и заканчивая оформлением и словечками "броузер", "плугин", "Богатая Интернет-аппликация".
А вообще, весь сайт выглядит как попытка троллинга — и надо признать, попытка удалась.
caustique, я не хотел никого задеть своим сайтом, простите меня! Просто я уже дошёл до той точки, когда надо остановиться в "освоении новых технологий".
Пойми правильно: хотя у автора и русские имя/фамилия, он, судя по всему, всю жизнь жил в Латвии, где общаются в-основном на латышском языке. Не суди его так строго.
Я никогда не пойму такие комменты, блоги типа "я инастраниц. учущийся руски" набирают по стопицот рейтинга, а если чел из стран бывшего СССР сделал пару ошибок, то сразу же кидают в него камнями.
Да при чем тут грамматические ошибки? Сайт сделан нелепо — верстка отвратительная, шрифты ужасные, все просто кошмарное, а автор утверждает, что так оно и надо. Все фразы что на сайте, что в посте написаны в стиле Lurkmore. Программа, которую автор рекламирует, мало того что ни черта не работает и ничего не доказывает, так еще и умеет ужасный интерфейс. Если бы автору было 15 лет, я бы с пониманием отнесся к его достижениям, но ему судя по ссылке на сайт бега 27 лет и в этом возрасте уже можно было бы сделать что-то приличное.
caustique, день добрый! Я не согласен с Вашим заявлением про схожесть стиля моего сайта и упомянутого Вами (анти)ресурса. Поясню. Упомянутый (анти)ресурс изначально нацелен на то, чтобы оскорбить кого-то, задеть. Мой сайт на это не рассчитан. Повторно прошу меня простить, если вёрстка HTML и/или CSS Вас лично задела за живое. Дизайн моего ресурса противоречит нескольким базовым "понятиям" "современного" веб-"дизайна". Я это не отрицаю. Из этого, тем не менее, не следует напрямую, что сайт отвратителен. Всё зависит от вкуса (или его отсутствия). Простите также, что я, как нижестоящий по званию кодер, позволяю себе такие вылазки в Ваш адрес. Но на сопках Маньчжурии тоже в бой пошёл оркестр, тут ничего не сделаешь.
Попробовал снять несколько галочек во вкладке Methods — сходу не помогло, пришлось перезапускать программу, чтобы изменить настройки методов. После этого снял галочку с закона исключенного третьего (excluded middle) и попытался доказать (p→¬p)→¬p. Программа зависла, а потом упала с комментарием в логе "Java heap space".
И сколько?
И сколько? 1000 EUR. Продано 0 лицензий.
Попробовал снять несколько галочек во вкладке Methods — сходу не помогло, пришлось перезапускать программу, чтобы изменить настройки методов. После этого снял галочку с закона исключенного третьего (excluded middle) и попытался доказать (p→¬p)→¬p. Программа зависла, а потом упала с комментарием в логе "Java heap space". Руководитель работы как-то доказал через программу закон Пирса, но не до конца -- свалилась на "Java stack size", если меня не глючит -- уже после построения доказательства программа не смогла его "развернуть" в "понятный пользователю вид". Почему пришлось перезапускать -- не знаю, возможно, много кликали одновременно, и я налажал с поточностью.