5 citations · 6 across the 4 of their papers we have counts for
5 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…
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.
Resource Adaptive Agents in Interactive Theorem Proving
Christoph Benzmueller, Volker Sorge
We introduce a resource adaptive agent mechanism which supports the user in interactive theorem proving. The mechanism uses a two layered architecture of agent societies to suggest…
LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)
Christoph Benzmueller, John Harrison, Carsten Schuermann
This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and…