Cesare Tinelli's Publications
Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump and Clark Barrett. Comparing Proof Systems for Linear Real Arithmetic with LFSC. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT'10), Edinburgh, UK, 2010.
Abstract. LFSC is a high-level declarative language for defining proof systems and proof objects for virtually any logic. One of its distinguishing features is its support for computational side conditions on proof rules. Side conditions facilitate the design of proof systems that reflect closely the sort of high-performance inferences made by SMT solvers. This paper investigates the issue of balancing declarative and computational inference in LFSC focusing on (quantifier-free) Linear Real Arithmetic. We discuss a few alternative proof systems for LRA and report on our comparative experimental results on generating and checking proofs in them.