| An efficient proof assistant uses a wide range of decision procedures, including automatic verification of validity of arithmetical formulas with linear terms. Since the final product of a proof assistant is a formalized and verified proof, it prompts an additional task of building proofs of formulas, which validity is established by such a decision procedure.; We present an implementation of several decision procedures for arithmetical formulas with linear terms in the MetaPRL proof assistant in a way that provides formal proofs of formulas found valid by those procedures.; We also present an implementation of a theorem prover for the logic of justified common knowledge S4Jn introduced in [Artemov, 2004]. This system captures the notion of justified common knowledge, which is free of some of the deficiencies of the usual common knowledge operator, and is yet sufficient for the analysis of epistemic problems where common knowledge has been traditionally applied. In particular, S4Jn enjoys cut-elimination, which introduces the possibility of automatic proof search in the logic of common knowledge. Our implementation automatically builds cut-free sequent proofs in S4Jn . This prover is based on the existing matrix-based prover for intuitionistic logic [Schmitt et al., 2001]. |
