Demuba3

A Automatic Demonstrator written in Prolog

Copyright (C) 2022 David Emmanuel Lopez

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program.  If not, see <https://www.gnu.org/licenses/>.

Introducción

Este repositorio corresponde a la implementación del trabajo de Tesis de David Emmanuel Lopez, "Heurísticas para la Demostración Automática basado en SNR", para la carrera Ingenieria de Sistemas. Para conocer en detalle el método, debe dirigirse a la documentación en /doc.

Instrucciones para testeo

• Primero, compile los predicados externos con compile.sh o compile.bat. Debe tener instalado SWI-Prolog. Para Ubuntu Linux, puede usar apt-get install swi-prolog para instalarlo.

• Ejecute demuba3 con demuba3.sh; el script carga la biblioteca externa y consulta demuba3.pl.

• Realice una consulta, como /- -(a & b) v (a & b):L.. La consulta de ejemplo pregunta si la fórmula -(a & b) v (a & b) es una tautología; la variable L devuelve el número de reglas utilizadas por el demostrador. Cuando se devuelve éxito (tautología), es para experimentos de rendimiento.

• Para pruebas por lotes, puede usar ./tester --dem=demuba3 --indexlib=index --set=c2670 --type=demostrart --limit=130 como ejemplo. El tester debe compilarse antes. En este ejemplo, se usará el demostrador demuba3.pl, se usará la biblioteca index.so/.dll para probar el caso de prueba tests/c2670 creado por iscas85_formula_generator. El tipo de prueba es demostrart; en este tipo de prueba, cada fórmula de los casos de prueba se usará como F v -F para generar tautologías. limit especifica el número de casos de prueba leídos del conjunto de pruebas.