{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:29:24Z","timestamp":1725748164435},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405365"},{"type":"electronic","value":"9783642405372"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40537-2_14","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T12:33:51Z","timestamp":1378902831000},"page":"149-156","source":"Crossref","is-referenced-by-count":7,"title":["Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"14_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.M. Andreoli","year":"1992","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Logic Comput.\u00a02(3), 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M. Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-25379-9_13","volume-title":"Certified Programs and Proofs","author":"F. Besson","year":"2011","unstructured":"Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 151\u2013166. Springer, Heidelberg (2011)"},{"key":"14_CR4","unstructured":"Farooque, M., Graham-Lengrand, S.: Sequent calculi with procedure calls. Technical report, Laboratoire d\u2019Informatique de l\u2019Ecole Polytechnique (January 2013), \n                    \n                      http:\/\/hal.archives-ouvertes.fr\/hal-00779199"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Farooque, M., Graham-Lengrand, S., Mahboubi, A.: A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. In: Momigliano, A., Pientka, B., Pollack, R. (eds.) Proceedings of the 2013 International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2013), Boston, USA. ACM Press (September 2013)","DOI":"10.1145\/2503887.2503892"},{"issue":"1","key":"14_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoret. Comput. Sci.\u00a050(1), 1\u2013101 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M.J. Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, R.J., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"14_CR8","unstructured":"The Isabelle theorem prover, \n                    \n                      http:\/\/isabelle.in.tum.de\/"},{"issue":"6","key":"14_CR9","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. of the ACM Press\u00a053(6), 937\u2013977 (2006)","journal-title":"J. of the ACM Press"},{"key":"14_CR10","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL 2010. EPiC Series, vol.\u00a02, pp. 1\u201311. EasyChair (2012)"},{"key":"14_CR11","unstructured":"Psyche: the Proof-Search factorY for Collaborative HEuristics, \n                    \n                      http:\/\/www.lix.polytechnique.fr\/~lengrand\/Psyche\/"},{"issue":"5","key":"14_CR12","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T. Weber","year":"2011","unstructured":"Weber, T.: SMT solvers: New oracles for the HOL theorem prover. International Journal on Software Tools for Technology Transfer (STTT)\u00a013(5), 419\u2013429 (2011)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40537-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T05:46:16Z","timestamp":1558071976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40537-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405365","9783642405372"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40537-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}