5 citations · 10 across the 4 of their papers we have counts for
4 papers
Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study
Christoph Benzmueller
In a case study we investigate whether off the shelf higher-order theorem provers and model generators can be employed to automate reasoning in and about quantified multimodal logi…
Quantified Multimodal Logics in Simple Type Theory
Christoph Benzmueller, Lawrence C. Paulson
We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification…
Granularity-Adaptive Proof Presentation
Marvin Schiller, Christoph Benzmueller
When mathematicians present proofs they usually adapt their explanations to their didactic goals and to the (assumed) knowledge of their addressees. Modern automated theorem prover…
A remark on higher order RUE-resolution with EXTRUE
Christoph Benzmueller
We show that a prominent counterexample for the completeness of first order RUE-resolution does not apply to the higher order RUE-resolution approach EXTRUE.