{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:21:25Z","timestamp":1759638085803},"reference-count":39,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,11,12]],"date-time":"2014-11-12T00:00:00Z","timestamp":1415750400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,1]]},"abstract":"<jats:p>In this paper, aimed at dependently typed programmers, we present a novel connection between automated and interactive theorem proving paradigms. The novelty is that the connection offers a better trade-off between usability, efficiency and soundness when compared to existing techniques. This technique allows for a powerful interactive proof framework that facilitates efficient verification of finite domain theorems and guided construction of the proof of infinite domain theorems. Such situations typically occur with industrial verification. As a case study, an embedding of SAT and CTL model checking is presented, both of which have been implemented for the dependently typed proof assistant Agda.<\/jats:p><jats:p>Finally, an example of a real world railway control system is presented, and shown using our proof framework to be safe with respect to an abstract model of trains not colliding or derailing. We demonstrate how to formulate safety directly and show using interactive theorem proving that signalling principles imply safety. Therefore, a proof by an automated theorem prover that the signalling principles hold for a concrete system implies the overall safety. Therefore, instead of the need for domain experts to validate that the signalling principles imply safety they only need to make sure that the safety is formulated correctly. Therefore, some of the validation is replaced by verification using interactive theorem proving.<\/jats:p>","DOI":"10.1017\/s0960129514000140","type":"journal-article","created":{"date-parts":[[2014,11,12]],"date-time":"2014-11-12T08:36:27Z","timestamp":1415781387000},"page":"129-153","source":"Crossref","is-referenced-by-count":6,"title":["A light-weight integration of automated and interactive theorem proving"],"prefix":"10.1017","volume":"26","author":[{"given":"KARIM","family":"KANSO","sequence":"first","affiliation":[]},{"given":"ANTON","family":"SETZER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,11,12]]},"reference":[{"key":"S0960129514000140_ref20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021923116629"},{"key":"S0960129514000140_ref14","volume-title":"Vorlesungen \u00fcber Zahlentheorie","author":"Dedekind","year":"1863"},{"key":"S0960129514000140_ref12","first-page":"29","article-title":"The mathematical language AUTOMATH, its usage, and some of its extensions.","volume":"125","author":"de Bruijn","year":"1970","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"S0960129514000140_ref27","volume-title":"RAILWAY Control Systems","author":"Leach","year":"2003"},{"key":"S0960129514000140_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_8"},{"key":"S0960129514000140_ref30","volume-title":"Railway Signalling","author":"Nock","year":"2002"},{"key":"S0960129514000140_ref36","unstructured":"Verma K. N. (2000) Reflecting Symbolic Model Checking in coq , Master's thesis, M\u00e9moire de DEA, DEA Programmation, Paris."},{"key":"S0960129514000140_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"S0960129514000140_ref38","unstructured":"Woodbridge P. (2011) Locking frame testing. Available at http:\/\/www.signalbox.org\/branches\/pw\/index.htm"},{"key":"S0960129514000140_ref13","doi-asserted-by":"crossref","unstructured":"De Moura L. and Bj\u00f8rner N. (2009) Satisfiability modulo theories: An appetizer. In: Formal Methods: Foundations and Applications 23\u201336.","DOI":"10.1007\/978-3-642-10452-7_3"},{"key":"S0960129514000140_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"S0960129514000140_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"S0960129514000140_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863560"},{"key":"S0960129514000140_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9143-8"},{"key":"S0960129514000140_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BF00485463"},{"key":"S0960129514000140_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275"},{"key":"S0960129514000140_ref3","unstructured":"Bar-Hillel Y. , Perles M. and Shamir E. (1964) On formal properties of simple phrase structure grammars. In: Language and Information: Selected Essays on their Theory and Application 116\u2013150."},{"key":"S0960129514000140_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_10"},{"key":"S0960129514000140_ref24","unstructured":"Kanso K. (2008) Formal Verification of Ladder Logic, Master's thesis, Department of Computer Science, Swansea University."},{"key":"S0960129514000140_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"S0960129514000140_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.015"},{"key":"S0960129514000140_ref31","volume-title":"Programming in Martin-L\u00f6f's Type Theory","author":"Nordstr\u00f6m","year":"1990"},{"key":"S0960129514000140_ref16","unstructured":"Dong Y. , Ramakrishnan C. R. and Smolka S. A. (2003) Model checking and evidence exploration. In: Proceedings of 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems 214\u2013223."},{"key":"S0960129514000140_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_32"},{"key":"S0960129514000140_ref9","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.20.11.584"},{"key":"S0960129514000140_ref10","volume-title":"Combinatory Logic","author":"Curry","year":"1958"},{"key":"S0960129514000140_ref19","first-page":"111","article-title":"Automated and interactive theorem proving.","volume":"14","author":"Harrison","year":"2008","journal-title":"NATO Science for Peace and Security Series"},{"key":"S0960129514000140_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_11"},{"key":"S0960129514000140_ref26","volume-title":"Introduction to Railway Signalling","author":"Kerr","year":"2001"},{"key":"S0960129514000140_ref28","unstructured":"Lescuyer S. and Conchon S. (2008) A reflexive formalization of a SAT solver in coq. In: TPHOLs 2008: Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics."},{"key":"S0960129514000140_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.007"},{"key":"S0960129514000140_ref4","first-page":"737","volume-title":"Handbook of Satisfiability","author":"Barrett","year":"2009"},{"key":"S0960129514000140_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"S0960129514000140_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_1"},{"key":"S0960129514000140_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.121"},{"key":"S0960129514000140_ref11","doi-asserted-by":"publisher","DOI":"10.2307\/1970289"},{"key":"S0960129514000140_ref21","first-page":"479","article-title":"The formulae-as-types notion of construction.","volume":"44","author":"Howard","year":"1980","journal-title":"To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism"},{"key":"S0960129514000140_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014565"},{"key":"S0960129514000140_ref23","unstructured":"Jones C. B. , Grov G. and Bundy A. (2010) Ideas for a high-level proof strategy language, Technical Report CS-TR-1210, Newcastle University."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000140","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T08:11:08Z","timestamp":1566029468000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000140\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,12]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,1]]}},"alternative-id":["S0960129514000140"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000140","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,12]]}}}