Colección de problemas para la demostración automática de teoremas
TPTP (Thousands of Problems for Theorem Provers) [1] es una colección de problemas de libre acceso para la demostración automática de teoremas . Se utiliza para evaluar la eficacia de los algoritmos de razonamiento automático. [2] [3] [4] Los problemas se expresan en un formato simple basado en texto para la lógica de primer orden o la lógica de orden superior. [5] TPTP se utiliza como fuente de algunos problemas en CASC .
Referencias
- ^ "La biblioteca de problemas TPTP para la demostración automatizada de teoremas".
- ^ Hoder, Kryštof; Voronkov, Andrei (2009). "Comparación de algoritmos de unificación en la demostración de teoremas de primer orden". KI 2009: Avances en inteligencia artificial . Apuntes de clase en informática. Vol. 5803. págs. 435–443. CiteSeerX 10.1.1.329.1809 . doi :10.1007/978-3-642-04617-9_55. ISBN . 978-3-642-04616-2.
- ^ Hurd, Joe (2003). "Tácticas de prueba de primer orden en demostradores de teoremas de lógica de orden superior". S2CID 11201048.
- ^ Segre, Alberto Maria; Sturgill, David B. (1994). "Uso de cientos de estaciones de trabajo para resolver problemas de lógica de primer orden" (PDF) . Actas de la AAAI-94 .
- ^ Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff (2008). "THF0: el núcleo del lenguaje TPTP para la lógica de orden superior". Razonamiento automatizado . Apuntes de clase en informática. Vol. 5195. págs. 491–506. doi :10.1007/978-3-540-71070-7_41. ISBN 978-3-540-71069-1.
Enlaces externos
