مقاله Extending Sledgehammer with SMT Solvers : تی پی بین

خلاصه مقاله

Sledgehammer is a component of Isabelle/HOL that employs resolution-based first-order automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically selects relevant facts and, if an ATP is successful, produces a snippet that replays the proof in Isabelle. We extended Sledgehammer to invoke satisfiability modulo theories (SMT) solvers as well, exploiting its relevance filter and parallel architecture. The ATPs and SMT solvers nicely complement each other, and Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs’ reach.

نویسندگان

Jasmin Christian Blanchette [ Institut für Informatik, Technische Universität München, Munich, Germany ]

Sascha Böhme [ Institut für Informatik, Technische Universität München, Munich, Germany ]

Lawrence C. Paulson [ Computer Laboratory, University of Cambridge, Cambridge, UK ]

کلمات کلیدی

SMT solvers Automatic theorem provers Interactive theorem provers

آدرس این مقاله

آدرس مستقیم دسترسی به این مقاله

مشخصات کنفرانس

مشاهده مقالات

Journal of Automated Reasoning 2013

The interdisciplinary Journal of Automated Reasoning balances theory, implementation and application. The spectrum of coverage ranges from the presentation of a new inference rule with proof of its logical properties to a detailed account of a computer program designed to solve various problems in industry. Topics include automated theorem proving, logic programming, expert systems, program synthesis and validation, artificial intelligence, computational logic, robotics, and various industrial applications. The contents focus on several aspects of automated reasoning, a field whose objective is the design and implementation of a computer program that serves as an assistant in solving problems and in answering questions that require reasoning. The Journal of Automated Reasoning provides a forum and a means for exchanging information for those interested purely in theory, those interested primarily in implementation, and those interested in specific research and industrial applications.

حوزه های تحت پوشش : automated theorem proving, logic programming, expert systems, program synthesis and validation, artificial intelligence, computational logic, robotics, and various industrial applications