Jump to content

Semantic resolution tree

From Wikipedia, the free encyclopedia
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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]

References

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