A Usability Evaluation of Interactive Theorem Provers Using Focus Groups

A primary goal of the usability evaluation process is to create interfaces that can be seamlessly integrated into current processes and create an enjoyable experience for the user. Given this, it is critical to capture user input to effectively drive product development and redesign. While many methods are available to usability practitioners, this paper highlights three techniques that can be used to substantially enhance usability evaluation output. Specifically this paper presents a method to utilize focus groups, emotional profiling and Kano analysis methods in combination to define user needs, expectations, and desires, provide an explanation of why features of a product are liked or disliked, as well as add additional structure to the prioritization of usability shortcomings and related redesign recommendations. A background on each method, the process for implementing them into usability analyses, and guidelines for successful use are provided for usability practitioners.

Download Full-text

Checkable Proofs for First-Order Theorem Proving

10.29007/s6d1 ◽

2018 ◽

Author(s):

Giles Reger ◽

Martin Suda

Keyword(s):

Theorem Proving ◽

Critical Mass ◽

Current Situation ◽

Boolean Satisfiability ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Theorem Provers ◽

Interactive Theorem Provers ◽

Theory Reasoning

Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),we argue that a similar goal of having unified automatically checkable proofs should be soughtby the developers of automated first-order theorem provers (ATPs). This would not onlyhelp to further increase assurance about the correctness of prover results,but would also be indispensable for tools which rely on ATPs,such as ``hammers'' employed within interactive theorem provers.The current situation, represented by the TSTP format is unsatisfactory,because this format does not have a standardised semantics and thus cannot be checked automatically.Providing such semantics, however, is a challenging endeavour. One would ideallylike to have a proof format which covers only-satisfiability-preserving operations such as Skolemisationand is versatile enough to encompass various proving methods (i.e. not just superposition)or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.Going beyond pure first-order logic to theory reasoning in the style of SMT orbeyond proofs to certification of satisfiability are further interesting challenges.Although several projects have already provided partial solutions in this direction,we would like to use the opportunity of ARCADE to further promote the idea andgather critical mass needed for its satisfactory realisation.

Download Full-text

The Next Generation of Interactive Theorem Provers

7th International Conference on Automated Deduction - Lecture Notes in Computer Science ◽

10.1007/978-0-387-34768-4_18 ◽

1984 ◽

pp. 303-315 ◽

Cited By ~ 2

Author(s):

Patrick Suppes

Keyword(s):

Next Generation ◽

Theorem Provers ◽

Interactive Theorem Provers

Download Full-text

Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers

10.29007/36dt ◽

2018 ◽

Cited By ~ 2

Author(s):

Lawrence C. Paulson ◽

Jasmin Christian Blanchette

Keyword(s):

Years Of Experience ◽

Interactive Proof ◽

Theorem Provers ◽

Proof Construction ◽

Interactive Theorem Provers ◽

Automatic Theorem Provers ◽

Automatic Theorem

Sledgehammer is a highly successful subsystem of Isabelle/HOL that calls automatic theorem provers to assist with interactive proof construction. It requires no user configuration: it can be invoked with a single mouse gesture at any point in a proof. It automatically finds relevant lemmas from all those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle/HOL proof scripts: its output cannot be trusted, but it does not need to be trusted. Sledgehammer works well with Isar structured proofs and allows beginners to prove challenging theorems.

Download Full-text