Semantic resolution tree explained

A semantic resolution tree is a tree used for the definition of the semantics of a programming language.^[1] They have often been used as a theoretical tool for showing the unsatisfiability of clauses in first-order predicate logic.^[2]

Notes and References

1. Book: Kundu, S. Proceedings of the ACM SIGART international symposium on Methodologies for intelligent systems. Tree resolution and generalized semantic tree. 1986-12-01. https://doi.org/10.1145/12808.12838. ISMIS '86. Knoxville, Tennessee, USA. Association for Computing Machinery. 270–278. 10.1145/12808.12838. 978-0-89791-206-8. 17442587.
2. Kim. Choon Kyu. Newborn. Monty. 2003. Dongarra. Jack. Laforenza. Domenico. Orlando. Salvatore. Competitive Semantic Tree Theorem Prover with Resolutions. Recent Advances in Parallel Virtual Machine and Message Passing Interface. Lecture Notes in Computer Science. 2840 . en. Berlin, Heidelberg. Springer. 227–231. 10.1007/978-3-540-39924-7_33. 978-3-540-39924-7.