{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:51Z","timestamp":1761611331377},"reference-count":21,"publisher":"Wiley","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"unspecified","delay-in-days":2953,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["LMS J. Comput. Math."],"published-print":{"date-parts":[[2002]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A generalisation of Milner's \u2018LCF approach\u2019 is described. This allows algorithms based on binary decision diagrams (BDDs) to be programmed as derived proof rules in a calculus of representation judgements. The derivation of representation judgements becomes an LCF-style proof by defining an abstract type for judgements analogous to the LCF type of theorems. The primitive inference rules for representation judgements correspond to the operations provided by an efficient BDD package coded in C (BuDDy). Proof can combine traditional inference with steps inferring representation judgements. The resulting system provides a platform to support a tight and principled integration of theorem proving and model checking. The methods are illustrated by using them to solve all instances of a generalised Missionaries and Cannibals problem.<\/jats:p>","DOI":"10.1112\/s1461157000000693","type":"journal-article","created":{"date-parts":[[2013,8,6]],"date-time":"2013-08-06T07:42:12Z","timestamp":1375774932000},"page":"56-76","source":"Crossref","is-referenced-by-count":13,"title":["Programming Combinations of Deduction and BDD-based Symbolic Calculation"],"prefix":"10.1112","volume":"5","author":[{"given":"Michael J. C.","family":"Gordon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2010,2,1]]},"reference":[{"key":"S1461157000000693_ref020","unstructured":"20 Seger Carl-Johan H. , \u2018VOSS - a formal hardware verification system: User's guide\u2019, Tech. Rep UBC TR 93\u201345, The University of British Columbia, (December, 1993)."},{"key":"S1461157000000693_ref018","article-title":"\u2018For mally verifying IEEE compliance of floating-point hardware\u2019","author":"O'Leary","journal-title":"Intel Technology J."},{"key":"S1461157000000693_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S1461157000000693_ref016","unstructured":"16 McMillan Ken , \u2018SMV\u2019, http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\/."},{"key":"S1461157000000693_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_6"},{"key":"S1461157000000693_ref005","first-page":"365","volume-title":"Automatic verification methods for finite state systems","author":"Coudert","year":"1989"},{"key":"S1461157000000693_ref021","unstructured":"21 International Sri , \u2018PVS\u2019, http:\/\/www.csl.sri.com\/pvs.html."},{"key":"S1461157000000693_ref006","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-44659-1_12","article-title":"\u2018Reachability programming in HOL98 using BDDs\u2019","author":"Gordon","year":"2000","journal-title":"International Conference on Theorem Proving and Higher Order Logics"},{"key":"S1461157000000693_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60045-0_42"},{"key":"S1461157000000693_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57826-9_135"},{"key":"S1461157000000693_ref013","unstructured":"13 McCarthy John , \u2018Elaboration tolerance\u2019, http:\/\/www-formal.stanford.edu\/jmc\/elaboration\/node2.html."},{"key":"S1461157000000693_ref008","article-title":"Edinburgh LCF","volume":"78","author":"Gordon","year":"1979","journal-title":"a mechanised logic of computation"},{"key":"S1461157000000693_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"S1461157000000693_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_22"},{"key":"S1461157000000693_ref012","unstructured":"12 Lee Trevor W.S. , Greenstreet Mark R. and Seger Carl-Johan , \u2018Automatic verification of asynchronous circuits\u2019, Tech. Rep. UBC TR 93\u201340, The University of British Columbia (November, 1993)."},{"key":"S1461157000000693_ref002","first-page":"131","volume-title":"Machine intelligence","volume":"3","author":"Amarel","year":"1971"},{"key":"S1461157000000693_ref003","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"S1461157000000693_ref004","volume-title":"Model checking","author":"Clarke","year":"1999"},{"key":"S1461157000000693_ref007","unstructured":"7 Gordon Mike , \u2018HolBddLib\u2019, http:\/\/www.cl.cam.ac.uk\/~mjcg\/HolBddLib\/."},{"key":"S1461157000000693_ref009","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.2.162"},{"key":"S1461157000000693_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63475-4_1"}],"container-title":["LMS Journal of Computation and Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1461157000000693","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T19:48:45Z","timestamp":1559936925000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1461157000000693\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"references-count":21,"alternative-id":["S1461157000000693"],"URL":"https:\/\/doi.org\/10.1112\/s1461157000000693","relation":{},"ISSN":["1461-1570"],"issn-type":[{"value":"1461-1570","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002]]}}}