Title :
Herbrand´s theorem, automated reasoning and semantic tableaux
Author :
Voronkov, Andrei
Author_Institution :
Dept. of Comput. Sci., Uppsala Univ., Sweden
Abstract :
We overview recent results related to Herbrand´s theorem and tableau-like methods of automated deduction and prove some new results. Based on an analysis and discussion of these results, new research directions are suggested
Keywords :
inference mechanisms; theorem proving; Herbrand´s theorem; automated deduction; automated reasoning; semantic tableaux; tableau-like methods; Boolean functions; Computational complexity; Data structures; Logic; Terminology;
Conference_Titel :
Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on
Conference_Location :
Indianapolis, IN
Print_ISBN :
0-8186-8506-9
DOI :
10.1109/LICS.1998.705662
