ABSTRACT. We describe the implementation of the alternating path method for premise selection in the theorem prover PyRes.

ABSTRACT. Metamath is an established computer language for archiving, verifying, and studying mathematical proofs. Its basis is condensed detachment, with unification and a view on proofs as terms. Grammar-based tree compression applied to such proof terms factorizes repeated patterns, which provide proofs of definite clauses, pattern variables corresponding to body atoms. A Metamath database is then just a grammar that compresses a set of giant proof trees. We provide a formal account of this view and have implemented a practical toolkit. In experiments we compare the proof structuring of Metamath by human experts with machine-generated structurings, and address possibilities of the interplay of both.

ABSTRACT. The diversity of output encodings of different reasoning systems hinders proof verification and interoperability. The Dedukti framework addresses this issue by implementing the λΠ-calculus modulo, enabling proofs from different frameworks to be expressed, combined, and checked automatically. We identify common challenges and requirements for verifying proofs of automated theorem provers for higher-order logic, and develop general strategies for systematically deriving encodings of calculus rules and proof steps. Building on these strategies, we propose a modular encoding approach, which we demonstrate and evaluate using the higher-order logic prover Leo-III. This effort has already led to the discovery and resolution of minor bugs in the original prover.

ABSTRACT. We present novel semiring semantics for abstract reduction systems (ARSs), i.e., a set A together with a binary relation → denoting reductions. More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring S = (S, ⊕, ⊙, 0, 1), which consists of a set S associated with two operations ⊕ and ⊙ with identity elements 0 and 1, respectively. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. For that reason, we consider semirings where the natural order (that is induced by addition of the semiring) forms a complete lattice. In most applications of semiring semantics in logic, a higher “truth value” w.r.t. the natural order is more desirable, e.g., for the confidence semiring Sconf = ([0, 1], max, ·, 0, 1) that can be used to assign confidence values to facts, one would like to obtain a value close to the most desirable confidence 1. However, in the application of software verification, it is often the reverse, e.g., for computing the runtime of a reduction via the arctic semiring Sarc = (N±∞, max, +, −∞, 0). While every runtime t < ∞ may still be acceptable, the aim is to prove boundedness, i.e., that the maximum ∞ (an infinite runtime) cannot occur. Our semiring semantics capture and generalize numerous formalisms that have been studied in the literature. For example, boundedness w.r.t. different semirings can imply termination of the underlying ARS, it can ensure that certain bad states cannot be reached (safety), etc. By considering tuples over different semirings, we can combine multiple analyses into a single combined framework analyzing combinations of properties, where simply performing each analysis separately fails. Due to our generalization of existing formalisms via our semiring semantics, we can now use techniques and ideas from, e.g., termination analysis, to prove boundedness or other properties (or combinations of properties) of reduction systems using a completely different semiring. We present sufficient conditions for boundedness and show that the interpretation method, a well-known method to, e.g., prove termination of ARSs, can be generalized to a sound (and sometimes complete) technique to prove boundedness. On the other hand, we also try to find worst-case lower bounds on weights in order to detect bugs and possible denial of service attacks.

ABSTRACT. n/a (the submission itself is a one-page abstract)