ABSTRACT. Interfacing with theorem provers is normally done by specifying a strategy. Such a strategy can be local, such as using tactics in interactive theorem provers, or global when using automatic ones. Focused proof calculi have a clear separation between the phases in the proof search which can be done fully automatically and those phases which require decision making. The inference rules of these proof calculi can be defined using logical formulas, such as implications. Logic programming languages allow for proof search over a database of such logical formulas and also support interaction with the user via input/output calls. In this paper we describe a possible process of writing an interactive proof assistant over a focused sequent calculus using the higher-order programming language lambda-prolog. We show that one can gain a high level of trust in the correctness of the prover, up to the correctness of an extremely small kernel. This process might allow one to obtain a fully functional proof assistant using a small amount of code and by using a clear process for arbitrary focused calculi.

ABSTRACT. Resolution and superposition are common techniques which have seen widespread use with propositional and first-order logic in modern theorem provers. In these cases, resolution proof production is a key feature of such tools; however, the proofs that they produce are not necessarily as concise as possible. For propositional resolution proofs, there are a wide variety of proof compression techniques. There are fewer techniques for compressing first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. One method for propositional proof compression is partial regularization, which removes an inference n when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from n to the root of the proof. This paper describes the generalization of the partial-regularization algorithm RecyclePivotsWithIntersection [10] from propositional logic to first-order logic. An empirical evaluation of the generalized algorithm and its combinations with the previously lifted GreedyLinearFirstOrderLowerUnits algorithm [12] is also presented.

ABSTRACT. Interactive program verification is characterized by iterations of unfinished proof attempts. For proof construction, many interactive program verification systems offer either text-based interactions, in using a proof scripting language, or a form of direct-manipulation interaction. We have combined a direct-manipulation program verification system with a text-based interface to leverage the advantages of both interaction paradigms. To give the user more insight when scripting proofs we have adapted well-known interaction concepts from the field of software debugging. In this paper we contribute with experiences from combining the direct-manipulation interface of the interactive program verification system KeY with a text-based user interface to construct program verification proofs leveraging interaction concepts from the field of software-debugging for the proof process.

ABSTRACT. We present a chat bot as an interface to the Coq proof assistant. It provides modern way of interaction with Coq across multiple devices. We emphasize that it runs on several platform, having not the same interface but similar, at the same time it employs features of particular device. Moreover it is also easy to run it on mobile devices with Android and iOS.

ABSTRACT. The beginnings of the Isabelle Prover IDE framework (Isabelle/PIDE) go back to the year 2008. This is a report on the project after 10 years, with system descriptions for various PIDE front-ends, namely (1) Isabelle/jEdit, the main PIDE application and default Isabelle user-interface, (2) Isabelle/VSCode, an experimental application of the Language Server Protocol in Visual Studio Code (by Microsoft), and (3) a headless PIDE server with JSON protocol messages over TCP sockets.

ABSTRACT. The System for Automated Deduction (SAD) by Andrei Paskevich proof-checks texts written in nearly natural mathematical language, without explicit system commands or prover commands. Natural language features like soft typing by noun phrases guide efficient text processing and proof checking. We have implemented practical improvements of the checking algorithm and extensions of the input language, so that we are now able to process considerably longer and more complicated texts. These are immediately readable by mathematicians, as demonstrated by subsequent examples. This suggests an approach to formal mathematics through collections or libraries of texts in (a controlled) natural language.