Journal article icon

Journal article

Tool building requirements for an API to first-order solvers

Abstract:

Effective formal verification tools require that robust implementations of automatic procedures for first-order logic and satisfiability modulo theories be integrated into expressive interactive frameworks for logical deduction, such as higher-order logic theorem provers. This paper states some pragmatic requirements for implementations of decision procedures that make them well-suited to integration into such frameworks. The aim is to open a dialogue with the designers of decision procedu...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Publisher's version

Actions


Access Document


Files:
Publisher copy:
10.1016/j.entcs.2005.12.003

Authors


More by this author
Institution:
University of Oxford
Department:
Mathematical, Physical & Life Sciences Division - Department of Computer Science
Role:
Author
Publisher:
Elsevier Publisher's website
Journal:
Electronic Notes in Theoretical Computer Science Journal website
Volume:
144
Issue:
2
Pages:
15–26
Publication date:
2006-01-08
DOI:
ISSN:
1571-0661
URN:
uuid:3536370c-6c28-48bf-a962-e0c5b8641766
Local pid:
ora:10652

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP