ICAIL
2003
ACM
14 years 5 months ago
2003
ACM
This paper proposes a logic-oriented framework for institutional agents specification and analysis. Within this framework institutional agents are seen as artificial agents that a...
TPHOL
2003
IEEE
14 years 5 months ago
2003
IEEE
Abstract. Model checking and theorem proving are two complementary approaches to formal verification. In this paper we show how binary decision diagram (BDD) based symbolic model ...
LPAR
2004
Springer
14 years 5 months ago
2004
Springer
Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. ...
ECAI
2004
Springer
14 years 5 months ago
2004
Springer
Attempts to use finite models to guide the search for proofs by resolution and the like in first order logic all suffer from the need to trade off the expense of generating and m...
VSTTE
2005
Springer
14 years 5 months ago
2005
Springer
How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and p...
TABLEAUX
2005
Springer
14 years 5 months ago
2005
Springer
The Intuitionistic Logic Theorem Proving (ILTP) Library provides a platfom for testing and benchmarking theorem provers for first-order intuitionistic logic. It includes a collect...
PEPM
2007
ACM
15 years 10 months ago
2007
ACM
programming languages community is vigorously pursuing ways to incorporate F!-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach ...