Efficient deduction in first order logic with equality by combining semantictableaux and integer programming
4РП — Обучение и мобилност на изследователи
- Период
- 1996-08-01 → 1997-07-31
- Финансиране от ЕС
- —
- Участници
- 2
- Схема
- RGI
Линиите свързват координатора с партньорите. За проекти отпреди 2014 г. CORDIS не винаги дава точни координати. Тези точки са на ниво град или държава.
Накратко на български
Автоматизираното логическо заключение се изследва чрез комбиниране на семантични таблици и целочислено програмиране, за да се провери дали дадена формула е изпълнима. Това помага за подобряване на системите за автоматизирано разсъждение и разширяването им към логика с равенство.
Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.
Цел на проекта
The basis of the proposed project is an Automated Reasoning system developed at the University of Karlsruhe, that makes use of the idea of combining semantic tableaux and integer programming (IP): A formula (propositional or first-order) is transformed into an IP problem, and then IP methods are used to check whether the formula is satisfiable. The objective of this project is to extend the existing implementatio] (available when the project starts) and to unveil strongholds and problems of the method. Strategies and heuristics will be developed to utilize advantages, overcome problems and, thus, improve the method. This is an important and critical phase in the development of an Automated Reasoning system - even more in this case, since a calculus is implemented that has not been used before. In addition, a method will be developed for extending the combination of semantic tableaux and IP to handle first-order logic with equality.
Оригинален текст от CORDIS (на английски).
Участници
- IMPERIAL COLLEGE OF SCIENCE, TECHNOLOGY AND MEDICINE · LONDONКоординаторОбединеното кралство
- Not availableНиво градГермания
Връзки
Данни: CORDIS, © Европейски съюз