{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:20Z","timestamp":1725663800240},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540545071"},{"type":"electronic","value":"9783540384205"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54507-7_1","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:55:46Z","timestamp":1330210546000},"page":"1-10","source":"Crossref","is-referenced-by-count":4,"title":["User-oriented theorem proving with the ATINF graphic proof editor"],"prefix":"10.1007","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel","family":"Herment","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Zabel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader, H-J. B\u00fcrckert, B. Hollunder, W. Nutt, J.H. Siekmann: Concept logics in \u201cComputational logic\u201d (J.W. Lloyd ed.) Springer-Verlag 1990, pp. 177\u2013201.","DOI":"10.1007\/978-3-642-76274-1_10"},{"key":"1_CR2","unstructured":"T. Boy de la Tour, R. Caferra: Proof analogy in interactive theorem proving: a method to use and express it via second order pattern matching. Proc. AAAI-87, Morgan and Kaufmann 1987, pp. 95\u201399."},{"key":"1_CR3","unstructured":"T. Boy de la Tour, R. Caferra: L'analogie en d\u00e9monstration automatique: une approche de la g\u00e9n\u00e9ralisation utilisant le filtrage du second ordre. Actes 6\u00e8me RFIA. Tome 2. Dunod Informatique, 1987, pp. 809\u2013818."},{"key":"1_CR4","first-page":"558","volume":"449","author":"T. B. Tour de la","year":"1990","unstructured":"T. Boy de la Tour: Minimizing the number of clauses by renaming. Proc. of CADE-10, LNAI 449, Springer-Verlag 1990, pp. 558\u2013572.","journal-title":"LNAI"},{"key":"1_CR5","first-page":"402","volume":"358","author":"T. B. Tour de la","year":"1988","unstructured":"T. Boy de la Tour, R. Caferra: A formal approach to some usually informal techniques used in mathematical reasoning. Proc. of ISSAC-88. LNCS 358, Springer-Verlag 1988, pp. 402\u2013406.","journal-title":"LNCS"},{"key":"1_CR6","first-page":"744","volume":"310","author":"T. B. Tour de la","year":"1988","unstructured":"T. Boy de la Tour, R. Caferra, G. Chaminade: Some tools for an Inference Laboratory (ATINF). Proc. of CADE-9, LNCS 310, Springer-Verlag 1988, pp. 744\u2013745.","journal-title":"LNCS"},{"key":"1_CR7","unstructured":"T. Boy de la Tour, R. Caferra, G. Chaminade: Towards an inference laboratory. Proc. of COLOG-88 (International Conference in Computer Logic) P. Lorents, G. Mints and E. Tyugu eds., part II, pp. 5\u201313."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour, G. Chaminade: The use of renaming to improve the efficiency of clausal theorem proving. Proc. AIMSA '90. North-Holland 1990, pp. 3\u201312.","DOI":"10.1016\/B978-0-444-88771-9.50007-6"},{"key":"1_CR9","first-page":"153","volume":"478","author":"R. Caferra","year":"1990","unstructured":"R. Caferra, N. Zabel: Extending resolution for model construction. Proc. of Logics in AI \u2014 JELIA '90, LNAI 478, Springer-Verlag 1990, pp. 153\u2013169.","journal-title":"LNAI"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"R. Caferra, N. Zabel: An application of many-valued logic to decide propositional S5 formulae: a startegy designed for a parameterized tableaux-based theorem prover. Proc. AIMSA '90, North-Holland 1990. pp. 23\u201332.","DOI":"10.1016\/B978-0-444-88771-9.50009-X"},{"key":"1_CR11","unstructured":"R. Caferra, S. Demri, M. Herment: Logic morphisms as a framework for backward transfer of lemmas and strategies in some modal and epistemic logics. To appear in Proc. of AAAI-91."},{"key":"1_CR12","unstructured":"R. Caferra, S. Demri, M. Herment: Logic-independent graphic proof edition: an application in structuring and transforming proofs. In preparation."},{"issue":"1","key":"1_CR13","first-page":"7","volume":"3","author":"G. Chaminade","year":"1989","unstructured":"G. Chaminade: An implementation oriented view of order-sorted resolution. Revue d'Intelligence Artificielle Vol. 3 (1), August 1989, pp. 7\u201330.","journal-title":"Revue d'Intelligence Artificielle"},{"key":"1_CR14","unstructured":"G.Chaminade: Int\u00e9gration et impl\u00e9mentation de m\u00e9canismes de d\u00e9duction naturelle dans les d\u00e9monstrateurs utilisant la r\u00e9solution. Ph.D. thesis. Institut National Polytechnique de Grenoble. Forthcoming (October 1991)."},{"key":"1_CR15","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand, G. Huet: The Calculus of Constructions, Information and Computation 76 (1988), pp. 95\u2013120.","journal-title":"Information and Computation"},{"key":"1_CR16","unstructured":"R. Constable et al.: Implementing mathematics with the Nuprl development system. Prentice-Hall 1986."},{"key":"1_CR17","unstructured":"P.J. Davis, R. Hersh: Descarte's dream. Harcourt Brace Jovanovich 1986."},{"key":"1_CR18","unstructured":"N.G. de Bruijn: A survey of the project AUTOMATH in \u201cTo H.B Curry: Essays on Combinatory Logic, Lambda calculus and formalism\u201d (J.P. Seldin and J.R. Hindley eds.) Academic Press 1980, pp. 579\u2013606."},{"key":"1_CR19","unstructured":"B. Delsart: General e-unification: balancing efficiency and complemeness. To be presented in Unif'91."},{"issue":"5","key":"1_CR20","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"R.A. Millo De","year":"1979","unstructured":"R.A. De Millo, R.J. Lipton, A.J. Perlis: Social processes and proofs of theorems and programs. Comm. of the ACM, Vol. 22, Number 5 (1979), pp. 271\u2013280.","journal-title":"Comm. of the ACM"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"M. Fitting: First-order logic and automated theorem proving. Springer-Verlag 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"issue":"5","key":"1_CR22","first-page":"77","volume":"11","author":"A.M. Frisch","year":"1991","unstructured":"A.M. Frisch, A.G. Cohn: Thoughts and Afterthoughts of the 1988 Workshop on principles of hybrid reasoning. AI Magazine, Vol. 11, Number 5, January 1991, pp. 77\u201383.","journal-title":"AI Magazine"},{"key":"1_CR23","unstructured":"R. Harper, F. Honsell, G. Plotkin: A framework for defining logics, Proc. of the 2nd Annual Logic in Computer Science, Ithaca, NY, 1987."},{"issue":"3","key":"1_CR24","first-page":"99","volume":"4","author":"T. K\u00e4ufl","year":"1990","unstructured":"T. K\u00e4ufl, N. Zabel: Cooperation of decision procedures in a tableau-based theorem prover. Revue d'Intelligence Artificielle. Special issue on Automated Deduction. Vol. 4 (3), November 1990, pp. 99\u2013125.","journal-title":"Revue d'Intelligence Artificielle"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"J. Mc Carthy: Computer programs for checking mathematical proofs. Proc. Amer. Math. Soc. Recursive Function Theory, 1961, pp. 219\u2013227.","DOI":"10.1090\/pspum\/005\/9998"},{"key":"1_CR26","first-page":"500","volume":"310","author":"H-J. Ohlbach","year":"1988","unstructured":"H-J. Ohlbach: A resolution calculus for modal logics. Proc. of CADE-9, LNCS 310, Springer-Verlag 1988, pp. 500\u2013516.","journal-title":"LNCS"},{"key":"1_CR27","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L.C. Paulson","year":"1989","unstructured":"L.C. Paulson: The foundations of a generic theorem prover. Journal of Automated Reasoning 5 (1989), pp. 363\u2013397.","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR28","unstructured":"F.J. Pelletier, P. Rudnicki: Non-Obviousness. AAR Newsletter No 6, September 1986, pp. 4\u20135."},{"issue":"1","key":"1_CR29","doi-asserted-by":"crossref","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, Vol. 12, No 1, January 1965, pp. 23\u201341.","journal-title":"Journal of the ACM"},{"issue":"4","key":"1_CR30","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P. Rudnicki","year":"1987","unstructured":"P. Rudnicki: Obvious inferences. Journal of Automated Reasoning. Vol. 3, No 4, December 1987, pp. 383\u2013393.","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR31","unstructured":"Wos L.: Automated Reasoning: 33 basic research problems. Prentice-Hall 1988."}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Artificial Intelligence Research"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54507-7_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:55:16Z","timestamp":1605646516000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54507-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540545071","9783540384205"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-54507-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}