ABSTRACT.  Satisfiability (SAT) solvers  have become powerful tools to solve a wide range of applications. In case SAT problems are satisfiable, it is easy to validate a witness. However, if SAT problems have no solutions, a proof of unsatisfiability is required to validate that result. Apart from validation, proofs of unsatisfiability are useful in several applications, such as interpolation and extracting a minimal unsatisfiable set  and in tools that use SAT solvers such as  theorem provers. We discuss the two main approaches for unsatisfiability proofs: resolution proofs and clausal proofs. Resolution proofs are used for several application, but they are hard to produce. Clausal proofs are easy to emit, but more costly to check. We compare both approaches, present how to produce and validate proofs, and provide some challenges regarding unsatisfiability proofs.

ABSTRACT. We discuss history, techniques, and challenges in producing and checking proofs from SMT solvers.

ABSTRACT. Interactive Theorem Provers have a long tradition, going back to the 1970s when interaction was introduced as a concept in computing. The main provers in use today can be traced back over 20-30 years of development. As common traits there are usually strong logical systems at the bottom, with many layers of add-on tools around the logical core, and big applications of formalized mathematics or formal methods. There is a general attitude towards flexibility and open-endedness in the combination of logical tools: typical interactive provers use automated provers and dis-provers routinely in their portfolio.

The subsequent exposition of interactive theorem proving (ITP) takes Isabelle/Isar as the focal point to explain concepts of the greater "LCF family'', which includes Coq and various HOL systems. Isabelle itself shares much of the relatively simple logical foundations of HOL, but follows Coq in the ambition to deliver a sophisticated system to end-users without requiring self-assembly of individual parts. Isabelle today is probably the most advanced proof assistant concerning its overall architecture and extra-logical infrastructure.

The "Isar'' aspect of Isabelle refers first to the structured language for human-readable and machine-checkable proof documents, but also to the Isabelle architecture that emerged around the logical framework in the past 10 years. Thus "Isabelle/Isar'' today refers to an advanced proof assistant with extra structural integrity beyond the core logical framework, with native support for parallel proof processing and asynchronous interaction in its Prover IDE (PIDE).