Semantic resolution tree

{{More references|date=December 2009}}

A semantic resolution tree is a tree used for the definition of the semantics of a programming language.{{Cite book|last=Kundu|first=S|title=Proceedings of the ACM SIGART international symposium on Methodologies for intelligent systems|chapter=Tree resolution and generalized semantic tree|date=1986-12-01|chapter-url=https://doi.org/10.1145/12808.12838|series=ISMIS '86|location=Knoxville, Tennessee, USA|publisher=Association for Computing Machinery|pages=270–278|doi=10.1145/12808.12838|isbn=978-0-89791-206-8|s2cid=17442587}} They have often been used as a theoretical tool for showing the unsatisfiability of clauses in first-order predicate logic.{{Cite journal|last1=Kim|first1=Choon Kyu|last2=Newborn|first2=Monty|date=2003|editor-last=Dongarra|editor-first=Jack|editor2-last=Laforenza|editor2-first=Domenico|editor3-last=Orlando|editor3-first=Salvatore|title=Competitive Semantic Tree Theorem Prover with Resolutions|url=https://link.springer.com/chapter/10.1007/978-3-540-39924-7_33|journal=Recent Advances in Parallel Virtual Machine and Message Passing Interface|series=Lecture Notes in Computer Science|volume=2840 |language=en|location=Berlin, Heidelberg|publisher=Springer|pages=227–231|doi=10.1007/978-3-540-39924-7_33|isbn=978-3-540-39924-7|url-access=subscription}}