LINUX.ORG.RU

Избранные сообщения runtime

Tech Talks @NSU — Автоматическое доказательство теорем

Форум — Development

Всем привет!

На следующей неделе у нас лекция для математиков и им сочувствующих.

18 ноября, 19:30: Автоматическое доказательство теорем (Ренат Идрисов, к.ф.-м.н., ИСИ СО РАН)

«Вы наверняка слышали, что в последнее время далеко не все теоремы доказываются вручную (вот, например, автоматизированный вывод свойств вероятностных алгоритмов, а вот полностью автоматическое доказательство всем известной теоремы о четырех красках).

Как именно работают системы автоматических доказательств и что за языки лежат в их основе? Похоже ли построение автоматических доказательств на программирование? Могу ли я доказывать свои любимые теоремы на C или C++?

В рамках лекции прозвучат ответы на эти и другие вопросы, а также будет проведен небольшой вводный инструктаж по Coq

Лекция пройдет в аудитории 223 нового спорткомплекса НГУ, вход свободный.

Онлайн-трансляция будет доступна вот тут: https://plus.google.com/events/cdtakpptlcidhk43o2sq7se3pqo

Все подробности, как всегда, на http://techtalks.nsu.ru

 ,

ymn ()

Разыскивается книга про то, как научиться программировать

Форум — Development

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

P.S. Стоит ли читать «SICP, HtDP, PCL», которые мне посоветовал анонимус?

 , , ,

evilmanul ()

Взгляните на запрос

Форум — Development
with recursive temp1 (id, parent_id, value, type)
as (
    select
        t1.id,
        t1.parent_id,
        t1.value::text,
        t1.type
    from address as t1
    where t1.id = 10
    union
    select
        t2.id,
        t2.parent_id,
        t2.value || ', ' || temp1.value,
        t2.type
    from address as t2 inner join temp1 ON (temp1.parent_id = t2.id)
)
select
    value
from temp1
where type > 'locality'
order by type desc
limit 1;

Добрый день, подскажите, пожалуйста, как сделать так, что t1.id можно было задавать через where ко всему выражению? (или как бы так его превратить во view?)

 , ,

Y ()

Помогите найти язык программирования

Форум — Development

Помогите пожалуйста найти язык программирования, в котором есть мощные средства метапрограммирования, но при этом он мог уметь генерировать высокопроизводительный код real-time приложений. Область применения - обработка видео потоков, рендеринг графики, элементы AI. Интерсуют именно возможности языка, а не наличие готовых библиотек и т.п. (приглянулся racket, но скорость...)

 , ,

elf80lvl ()

почему haskell используют совместно с erlang?

Форум — Development

Уже не в первый раз вижу миграцию с питона на haskell + erlang. Например, в яндексе и селектел. Зачем нужно сразу два яп?

 , ,

true_admin ()

Опубликован Google Common Lisp Style Guide

Форум — Development

Опубликован Google Common Lisp Style Guide:

http://google-styleguide.googlecode.com/svn/trunk/lispguide.xml

 , ,

gensym ()

Слава роботам!

Форум — Talks

Американская компания Rethink Robotics разработала робота, который может произвести настоящую революцию в промышленности. Механический рабочий по имени Бакстер (Baxter) создан специально для того, чтобы выполнять самую разнообразную работу на сборочных линиях.

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

http://www.vesti.ru/doc.html?id=912117&cid=2161

 

DNA_Seq ()

Oracle и Postgres: маны по диалектам и извращениям

Форум — Development

Господа,

Посоветуйте манов по сабжу, описывающих как можно больше всяких хитрых извращений с их базовым языком запросов (не касаясь тонкостей PL/SQL, например).

Цель: нужно будет узнать толк в разнице между разными версиями Оракла и Постгреса и портированием в точные эквиваленты между их базовым синтаксисом.

«Читай официальную документацию» - да, уже. Но к оффдокам хотелось бы еще какой-нибудь вдохновляющей литературы по теме.

(Пример: помню, была серия книжек какого-то хардкорного sql-щика, в которых рассказывалось, как закодить на sql всё что угодно от хэлловорлда и высоконагруженной базы до веб-приложения и анализатора текстов. А вот как зовут чувака и те книжки — уже не помню. Тогда это казалось такой ненужной ерундой. Да и сейчас, в общем-то... :).

Спасибо

UPD: хотя, если есть книжки аналогичного смвысла про PL/SQL и PL/pgSQL - тоже хотеть

stevejobs ()

Ментальные карты

Форум — Talks

Кто пользовался, какие плюсы и минусы? Linux тут при том, что поставил freemind, но не знаю зачем.

 

avertex ()

пролог в лиспе

Форум — Development

Привет.

Подскажите, в какой реализации лиспа хороший встроенный пролог?

Спасибо.

 ,

kvitaliy ()

Человеческое метапрограммирование

Форум — Development

Подскажите кто-нибудь ЯП с развитой метасистемой, только нормальный, а не лисп.

Ndulu ()

Книги по базам данных

Форум — Development

Решил заполнить пробелы в знаниях и почитать хорошей литературы по БД. Погуглил, видимо неплохой вариант - «Теория и практика построения баз данных (Д. Кренке)». Но, к сожалению, я что-то не смог найти ее в продаже (ни бумажной, ни электронной). Есть только в посредственном качестве в djvu. Vожет какую другую книгу посоветуете? Или знаете где эту добыть?

theos ()

Радиоэлектроника

Форум — Talks

Посоветуйте книжку по основам радиоэлектроники, которую можно скачать бесплатно без смс в правильном формате (fb2/epub)

nbdarvin ()

META 2012

Форум — Talks

Уже третий день как у нас в Переславле-Залесском на базе Института Программных Систем РАН (ИПС РАН) проходит третья международная конференция, посвященная метавычислениям: META2012.

Сайт конференции: http://meta2012.pereslavl.ru/

Краткий обзор тем конференции:

  • Дистилляция
  • Частичные вычисления
  • Смешанные вычисления
  • Инверсные вычисления
  • Суперкомпиляция
  • Окрестностное тестирование
  • Другие варианты применения вышеназванных методов в тестировании, верификации и обработке программ

Полный список докладов тут: http://meta2012.pereslavl.ru/papers/accepted-papers.html

Сборник в PDF: http://rghost.net/39087935

На странице с программой можно еще скачать презентации докладов Нила Джонса: http://meta2012.pereslavl.ru/program/program.html

// Скалофагам будет приятно знать, что в российских разработках, связанных с суперкомпиляцией, сейчас активно используется Scala.

// Докладов, в которых использовался бы Рефал на этой конференции, увы, нет.

 ,

buddhist ()

Помогите понять принцип решения задачи

Форум — Talks

Доброго времени суток! Есть задача и нет идеи как её решать. Гуглом пользовался, но получить внятного алгоритма так и не смог. Собственно, сама задача:

В крупном международном аэропорту во время пересадки встретились четверо туристов – Герман, Роман, Франк, и Свен. Их фамилии – Фишер, Нагель, Миллер и Шепард. Каждый из них путешествует из одной страны (Германия, Румыния, Франция, Швеция) в другую (Германия, Румыния, Франция, Швеция). Место отправления и место назначения каждого не совпадает с его именем. Определите, кого как зовут, откуда и куда они направляются. Известно, что:

1) Роман приехал не из Франции.

2) Герман направляется в страну, откуда приехал Фишер.

3) Свен приехал из страны, куда направляется Нагель.

4) Шепард приехал из страны, чье название совпадает с именем человека, который направляется во Францию.

5) Миллер направляется в страну, чье название совпадает с именем человека, который приехал оттуда, куда собрался Роман.

Заранее спасибо за помощь!

kirich ()

Java изменить директорию

Форум — Development

Как в java менять директорию в которой выполняется процесс?

 

TDrive ()