{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T06:32:24Z","timestamp":1769063544616,"version":"3.49.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[1993,9,1]],"date-time":"1993-09-01T00:00:00Z","timestamp":746841600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1993,9]]},"DOI":"10.1007\/bf01530803","type":"journal-article","created":{"date-parts":[[2005,4,19]],"date-time":"2005-04-19T00:24:51Z","timestamp":1113870291000},"page":"475-502","source":"Crossref","is-referenced-by-count":19,"title":["Embedding complex decision procedures inside an interactive theorem prover"],"prefix":"10.1007","volume":"8","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-9455-6","volume-title":"A Basis for Theoretical Computer Science","author":"M.A. Arbib","year":"1981","unstructured":"M.A. Arbib, A.J. Kfoury and R.N. Moll,A Basis for Theoretical Computer Science (Springer, New York, 1981)."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/77600.77617","volume":"37","author":"M. Abadi","year":"1990","unstructured":"M. Abadi and Z. Manna, Nonclausal deduction in first-order temporal logic, J. ACM 37(1990) 279?317.","journal-title":"J. ACM"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"P.B. Andrews, Theorem proving via general matings, J. ACM 28(1981)193?214.","journal-title":"J. ACM"},{"key":"CR4","unstructured":"J. Van Baalen, The role of reformulation in the automatic design of satisfiability procedures, in:Proc. Workshop on Change of Representation and Problem Reformulation, ed. M.R. Lowry (1992) pp. 161?172."},{"key":"CR5","unstructured":"R.S. Boyer and J.S. Moore,A Computational Logic, ACM Monograph Series (Academic Press, 1979)."},{"key":"CR6","first-page":"83","volume":"11","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. More, Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic, Machine Intelligence 11(1988)83?124.","journal-title":"Machine Intelligence"},{"key":"CR7","unstructured":"A. Bundy, A. Smaill and J. Hesketh, Turning eureka steps into calculations in automatic program synthesis, in:Proc. UK IT 90, ed. S.L.H. Clarke (1990) pp. 221?226. Also available from Edinburgh University as DAI Research Paper No. 448."},{"key":"CR8","unstructured":"R.L. Constable et al.,Implementing Mathematics with the NuPRL Proof Development System (Prentice-Hall, 1986)."},{"key":"CR9","unstructured":"A. Cimatti and F. Giunchiglia, Many sorted natural deduction, IRST Technical Report (1992), to appear."},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"N.G. deBruijn, The mathematical language automath, in:Symp. on Automatic Demonstration, Lecture Notes in Mathematics 125 (Springer, 1970) pp. 29?61.","DOI":"10.1007\/BFb0060623"},{"key":"CR11","unstructured":"B. Dreben and W.D. Goldfarb,The Decision Problem ? Solvable Classes of Quantificational Formulas (Addison-Wesley, 1979)."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour, Minimizing the number of clauses by renaming, in:Proc. 10th Conf. on Automated Deduction (Springer, 1990) pp. 558?572.","DOI":"10.1007\/3-540-52885-7_114"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam, A computer procedure for quantification theory, J. ACM 7(1960)201?215.","journal-title":"J. ACM"},{"key":"CR14","unstructured":"F. Giunchiglia and E. Giunchiglia, Building complex derived inference rules: a decider for the class of prenex universal-existential formulas, in:Proc. 7th Eur. Conf. on Artificial Intelligence (1988). Extended version available as DAI Research Paper No. 359, Department of Artificial Intelligence, Edinburgh University."},{"key":"CR15","volume-title":"Techical Report No. 9204-01","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia, The GETFOL Manual ? GETFOL Version 1, Techical Report No. 9204-01, DIST ? University of Genova, Genoa, Italy (1992). IRST Manual, IRST, Trento, Italy (forthcoming 1992)."},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"M.J. Gordon, A.J. Milner and C.P. Wadsworth,Edinburgh LCF ? A Mechanized Logic of Computation, Lecture Notes in Computer Science 78 (Springer, 1979).","DOI":"10.1007\/3-540-09724-4"},{"key":"CR17","volume-title":"Technical Report No. 9105-23","author":"F. Giunchiglia","year":"1991","unstructured":"F. Giunchiglia and P. Pecchiari, Riscrittura sintattica in GETFOL, Technical Report No. 9105-23, IRST, Trento, Italy (1991)."},{"key":"CR18","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0743-1066(89)90009-5","volume":"7","author":"G. Gallo","year":"1989","unstructured":"G. Gallo and G. Urbani, Algorithm for testing the satisfiability of propositional formulae, J. Logic Programming 7(1989)45?61.","journal-title":"J. Logic Programming"},{"key":"CR19","unstructured":"F. Harche, J.N. Hooker and G.L. Thompson, A computational study of satisfiability algorithms for propositional logic, Working Paper No. 1991-27 (1991)."},{"key":"CR20","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R.G. Jeroslow","year":"1990","unstructured":"R.G. Jeroslow and J. Wang, Solving propositional satisfiability problems, Ann. Math. Artificial Intelligence 1(1990)167?187.","journal-title":"Ann. Math. Artificial Intelligence"},{"key":"CR21","unstructured":"S.C. Kleene,Introduction to Metamathematics (North-Holland, 1952)."},{"key":"CR22","unstructured":"S.C. Kleene,Mathematical Logic (Wiley, 1967)."},{"key":"CR23","unstructured":"D.W. Loveland,Automated Theorem Proving: A Logical Basis (North-Holland, 1978)."},{"key":"CR24","unstructured":"S.J. Lee and D. A. Plaisted, Eliminating duplication with the hyper-linking strategy, Technical Report No. TR90-032, Department of Computer Science, University of North Carolina (1990)."},{"key":"CR25","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0004-3702(82)90011-X","volume":"18","author":"N.V. Murray","year":"1982","unstructured":"N.V. Murray, Completely non-clausal theorem proving, Artificial Intelligence 18(1982)67?85.","journal-title":"Artificial Intelligence"},{"key":"CR26","unstructured":"G. Nelson and D.C. Oppen, Simplification by cooperating decision procedures, Technical Report No. STAN-CS-78-652, Stanford Computer Science Department (1978)."},{"key":"CR27","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D.C. Oppen, Fast decision procedures based on congruence closure, J. ACM 27(1980) 356?364.","journal-title":"J. ACM"},{"key":"CR28","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"D.C. Oppen","year":"1980","unstructured":"D.C. Oppen, Reasoning about recursively defined data structures, J. ACM 27(1980)403?411.","journal-title":"J. ACM"},{"key":"CR29","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"F.J. Pelletier, Seventy-five problems for testing automatic theorem provers, J. Automated Reasoning 2(1986)191?216. See also Errata Corrige in J. Automated Reasoning 4(1988)235?236.","journal-title":"J. Automated Reasoning"},{"key":"CR30","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"D.A. Plaisted and S. Greenbaum, A structure-preserving clause form translation, J. Symb. Comput. 2(1986) 293?304.","journal-title":"J. Symb. Comput."},{"key":"CR31","volume-title":"Natural Deduction ? A Proof Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz,Natural Deduction ? A Proof Theoretical Study (Almquist and Wiksell, Stockholm, 1965)."},{"key":"CR32","unstructured":"W.V.O. Quine,Methods of Logic (Holt, New York, 1959)."},{"key":"CR33","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"A. Robinson","year":"1965","unstructured":"A. Robinson, A machine oriented logic based on the resolution principle, J. ACM 12(1965)23?41.","journal-title":"J. ACM"},{"key":"CR34","unstructured":"R. Shostak, An algorithm for reasoning about equality, in:Proc. 7th Int. Joint Conf. on Artificial Intelligence (1977) pp. 526?527."},{"key":"CR35","unstructured":"C. Walther, A many sorted calculus based on resolution and paramodulation, in:Proc. 8th Int. Joint Conf. on Artificial Intelligence (1983)."},{"key":"CR36","doi-asserted-by":"crossref","unstructured":"R.W. Weyhrauch, Prolegomena to a theory of mechanized formal reasoning, Artificial Intelligence, Special Issue on Non-monotonic Logic 13(1) (1980).","DOI":"10.1016\/0004-3702(80)90015-6"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01530803\/fulltext.html","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01530803.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01530803\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01530803","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T00:01:04Z","timestamp":1586217664000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01530803"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,9]]},"references-count":36,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1993,9]]}},"alternative-id":["BF01530803"],"URL":"https:\/\/doi.org\/10.1007\/bf01530803","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,9]]}}}