Árbol semántico
Method of analytic tableaux
- Fecha
- c. 1955 · fiabilidad media
- Lugar
- Ámsterdam, Holanda Septentrional, Países Bajos
- Autoría
- Evert Willem Beth
- Ámbito
- Saber y símbolos
Qué es
Procedimiento de prueba para lógica proposicional y de primer orden que construye un árbol de subfórmulas para probar o refutar una fórmula, y que además permite determinar la satisfacibilidad de conjuntos finitos de fórmulas; desarrollado por Evert Willem Beth.
A qué dio paso
- Base de la demostración automática de teoremas
- Uso en programación lógica y verificación de modelos
- Influencia en los resolutores SAT basados en tableaux