Hispanopedia WikiSPASS es un demostrador automático de teoremas para lógica de primer orden con igualdad, desarrollado en el Instituto Max Planck de Ciencias de la Computación y que utiliza el cálculo de superposición . Su nombre original significaba Synergetic Prover Augmenting Superposition with Sorts (Demostrador Sinérgico que Aumenta la Superposición con Tipos) . El sistema de demostración de teoremas se distribuye bajo la licencia FreeBSD . [ 1 ]
Una extensión de SPASS llamada SPASS-XDB añadió soporte para la recuperación en tiempo real de axiomas de unidades positivas desde fuentes externas. [ 2 ] De este modo, SPASS-XDB puede incorporar hechos procedentes de bases de datos relacionales , servicios web o servidores de datos enlazados . También se añadió soporte para operaciones aritméticas mediante Mathematica . [ 3 ]
Referencias
- ↑ "Max-Planck-Institut für Informatik - Automatización de la lógica: Spass" . Spass-prover.org . 28 de mayo de 2010 . Consultado el 10 de agosto de 2016 .
- ↑ Suda, Martin; Sutcliffe, Geoff; Wischnewski, Patrick; Lamotte-Schubert, Manuel; De Melo, Gerard (2009). «Fuentes externas de axiomas en la demostración automatizada de teoremas» . KI 2009: Avances en inteligencia artificial . Lecture Notes in Computer Science. Vol. 5803. pp. 281–288 . doi : 10.1007/978-3-642-04617-9_36 . ISBN 978-3-642-04616-2. Consultado el 10 de agosto de 2016 .
- ↑ David Stanovsky; Martin Suda; Geoff Sutcliffe. "SPASS-XDB se vuelve matemático" (PDF) . Karlin.mff.cuni.cz . Consultado el 10 de agosto de 2016 .
Fuentes
- Weidenbach, Christoph; Dimova, Dilyana; Fietzke, Arnaud; Kumar, Rohit; Suda, Martin; Wischnewski, Patrick (2009), "SPASS Versión 3.5", CADE -22: 22.ª Conferencia Internacional sobre Deducción Automatizada , Springer, pp. 140–145 .
Enlaces externos
- Sitio web oficial
- Demostradores de teoremas gratuitos
- Herramientas de programación Unix
- Instituto Max Planck de Informática