{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:15:17Z","timestamp":1766135717695},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540305538"},{"type":"electronic","value":"9783540316503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_18","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T09:44:25Z","timestamp":1132652665000},"page":"246-260","source":"Crossref","is-referenced-by-count":28,"title":["Automating Coherent Logic"],"prefix":"10.1007","author":[{"given":"Marc","family":"Bezem","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"18_CR1","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BF00881838","volume":"10","author":"A. Avron","year":"1993","unstructured":"Avron, A.: Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning\u00a010(2), 265\u2013281 (1993)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR2","unstructured":"Bezem, M.: Website for geometric logic, http:\/\/www.ii.uib.no\/~bezem\/GL"},{"key":"18_CR3","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1142\/9789812562494_0050","volume-title":"Current trends in Theoretical Computer Science","year":"2004","unstructured":"Bezem, M., Coquand, T.: Newman\u2019s Lemma \u2013 a Case Study in Proof Automation and Geometric Logic. In: Gurevich, Y. (ed.) The Logic in Computer Science Column. Bulletin of the European Association for Theoretical Computer Science, vol.\u00a079, pp. 86\u2013100 (February 2003); Also in Paun, G., Rozenberg, G., Salomaa, A. (eds.): Current trends in Theoretical Computer Science, vol.\u00a02, pp. 267\u2013282. World Scientific, Singapore (2004)"},{"issue":"3\u20134","key":"18_CR4","first-page":"253","volume":"29","author":"M.A. Bezem","year":"2003","unstructured":"Bezem, M.A., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. Journal of Automated Reasoning\u00a029(3\u20134), 253\u2013275 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR5","first-page":"57","volume":"36","author":"A. Blass","year":"1998","unstructured":"Blass, A.: Topoi and computation. Bulletin of the EATCS\u00a036, 57\u201365 (1998)","journal-title":"Bulletin of the EATCS"},{"key":"18_CR6","unstructured":"Bry, F., Torge, S.: Model generation for applications \u2013 A tableau method complete for finite satisfiability. Research Report PMS-FB-1997-15, LMU (1997)"},{"key":"18_CR7","unstructured":"Colmerauer, A., et al.: Un syst\u00e8me de communication homme-machine en fran\u00e7ais. Technical Report, Universit\u00e9 II Aix-Marseille (1973)"},{"key":"18_CR8","unstructured":"The Coq Development Team, The Coq Proof Assistant Reference Manual, Version 8.0. Available at, http:\/\/coq.inria.fr\/"},{"key":"18_CR9","unstructured":"Coquand, T.: A Completeness Proof for Geometric Logic. In: To appear in Proceedings LMPS 2003 (2003)"},{"issue":"2","key":"18_CR10","doi-asserted-by":"publisher","first-page":"219","DOI":"10.2307\/2031794","volume":"4","author":"A. Cronheim","year":"1953","unstructured":"Cronheim, A.: A proof of Hessenberg\u2019s Theorem. Proceedings of the AMS\u00a04(2), 219\u2013221 (1953)","journal-title":"Proceedings of the AMS"},{"issue":"3","key":"18_CR11","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/S0168-0072(01)00026-4","volume":"111","author":"M. Coste","year":"2001","unstructured":"Coste, M., Lombardi, H., Roy, M.F.: Dynamical methods in algebra: effective Nullstellens\u00e4tze. Annals of Pure and Applied Logic\u00a0111(3), 203\u2013256 (2001)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"18_CR12","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1093\/logcom\/14.2.117","volume":"14","author":"L. He","year":"2004","unstructured":"He, L., Chao, Y., Itoh, H.: R-SATCHMO: Refinements on I-SATCHMO. Journal of Logic and Computation\u00a014(2), 117\u2013143 (2004)","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"18_CR13","doi-asserted-by":"publisher","first-page":"14","DOI":"10.2307\/2268661","volume":"16","author":"A. Horn","year":"1951","unstructured":"Horn, A.: On sentences which are true of direct unions of algebras. Journal of Symbolic Logic\u00a016(1), 14\u201321 (1951)","journal-title":"Journal of Symbolic Logic"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Johnstone, P.: Sketches of an Elephant: a topos theory compendium. Oxford Logic Guides 44, vol.\u00a02. OUP (2002)","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"key":"18_CR15","unstructured":"Kowalski, R.A.: Predicate logic as a programming language. In: Proceedings IFIP 1974, pp. 569\u2013574 (1974)"},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00881861","volume":"14","author":"D. Loveland","year":"1995","unstructured":"Loveland, D., Reed, D., Wilson, D.: SATCHMORE: SATCHMO with RElevancy. Journal of Automated Reasoning\u00a014, 325\u2013351 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 415\u2013434. Springer, Heidelberg (1988)"},{"key":"18_CR18","unstructured":"Meier, A.: The proof transformation system TRAMP, http:\/\/www.ags.uni-sb.de\/~ameier\/tramp.html"},{"issue":"1","key":"18_CR19","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM\u00a012(1), 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"18_CR20","first-page":"103","volume-title":"Selected Works in Logic by Th. Skolem","year":"1970","unstructured":"Skolem, T.: Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit und Beweisbarkeit mathematischen S\u00e4tze nebst einem Theoreme \u00fcber dichte Mengen. In: Skrifter I, vol.\u00a04, pp. 1\u201336. Det Norske Videnskaps-Akademi (1920); Also in Fenstad, J.E. (ed.): Selected Works in Logic by Th. Skolem, pp. 103\u2013136. Universitetsforlaget, Oslo (1970)"},{"key":"18_CR21","volume-title":"Corrected reprint of the 1968 original","author":"R.M. Smullyan","year":"1995","unstructured":"Smullyan, R.M.: First-order logic. In: Corrected reprint of the 1968 original. Dover Publications Inc., New York (1995)"},{"key":"18_CR22","volume-title":"Term Rewriting Systems","author":"Terese","year":"2003","unstructured":"Terese: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"key":"18_CR23","unstructured":"Thousands of Problems for Theorem Provers, The TPTP Problem Library for Automated Theorem Proving, http:\/\/www.cs.miami.edu\/~tptp"},{"key":"18_CR24","unstructured":"Wielemaker, J.: SWI-Prolog 5.4.1 Reference Manual. Available at, http:\/\/www.swi-prolog.org\/"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T00:18:02Z","timestamp":1706746682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11591191_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}