Java and Web Extensions of the Yices Little Engine of Proof
Sokharith Sok · 2006
Automated Deduction, also known as Theorem Proving, is the study of pro-grams that prove theorems. The domain evolved into two main trends: uniform proof search procedures which are guided by heuristics and based on the John Alan Robinson’s resolution method, and combination of domain specific decision procedures called little engines of proof introduced by Hao Wang. Yices is a Satisfiability Modulo Theories little engine developed at Stanford Research Insti-tute (SRI) capable of handling theories including uninterpreted functions, inte-ger and real arithmetics, lambda expressions, arrays, bitvectors, tuples, records and recursive datatypes (e.g. lists). Yices is the 2006 winner of the Satisfiability Modulo Theories Competition (SMT-COMP), a competition that benchmarks the state-of-the-art little engines. Based on the needs expressed by the developers of Yices at SRI, for this Software Development and Engineering Master Thesis, we developed documen-tation and material to make Yices more accessible and encourage its use and