{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,10]],"date-time":"2024-01-10T00:01:45Z","timestamp":1704844905931},"reference-count":67,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1986,11,1]],"date-time":"1986-11-01T00:00:00Z","timestamp":531187200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[1986,11]]},"DOI":"10.1016\/0004-3702(86)90011-1","type":"journal-article","created":{"date-parts":[[2003,3,14]],"date-time":"2003-03-14T13:02:52Z","timestamp":1047646972000},"page":"117-263","source":"Crossref","is-referenced-by-count":11,"title":["An experimental logic based on the fundamental deduction principle"],"prefix":"10.1016","volume":"30","author":[{"given":"Frank M.","family":"Brown","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0004-3702(86)90011-1_BIB1","doi-asserted-by":"crossref","unstructured":"Andrews, P.B., private correspondence, June 26, 1984.","DOI":"10.1080\/13520806.1984.11759540"},{"key":"10.1016\/0004-3702(86)90011-1_BIB2","series-title":"International Computing Symposium","article-title":"Proof search in a Gentzen-like system of first order logic","author":"Bibel","year":"1975"},{"key":"10.1016\/0004-3702(86)90011-1_BIB3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","article-title":"Non-resolution theorem proving","volume":"9","author":"Bledsoe","year":"1977","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0004-3702(86)90011-1_BIB4","series-title":"A Computational Logic","author":"Boyer","year":"1979"},{"key":"10.1016\/0004-3702(86)90011-1_BIB5","series-title":"Proceedings 2nd AISB Conference","article-title":"A deductive system for elementary arithmetic","author":"Brown","year":"1976"},{"key":"10.1016\/0004-3702(86)90011-1_BIB6","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0004-3702(77)90019-4","article-title":"Doing arithmetic without diagrams","volume":"8","author":"Brown","year":"1977","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0004-3702(86)90011-1_BIB7","series-title":"Proceedings Fifth International Joint Conference on Artificial Intelligence","article-title":"A theorem prover for elementary set theory","author":"Brown","year":"1977"},{"key":"10.1016\/0004-3702(86)90011-1_BIB8","series-title":"Proceedings Fifth International Joint Conference on Artificial Intelligence","article-title":"Inductive reasoning in mathematics","author":"Brown","year":"1977"},{"key":"10.1016\/0004-3702(86)90011-1_BIB9","doi-asserted-by":"crossref","DOI":"10.1016\/S0004-3702(78)80017-4","article-title":"Towards the automation of set theory and its logic","volume":"10","author":"Brown","year":"1978","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0004-3702(86)90011-1_BIB10","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/0004-3702(79)90007-9","article-title":"Inductive reasoning on recursive equation","volume":"12","author":"Brown","year":"1979","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0004-3702(86)90011-1_BIB11","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0004-3702(80)90049-1","article-title":"An investigation into the goals of research in automatic theorem proving as related to mathematical reasoning","volume":"14","author":"Brown","year":"1980","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0004-3702(86)90011-1_BIB12","series-title":"Proceedings 3rd AISB\/GI Conference","article-title":"A sequent calculus for modal quantificational logic","author":"Brown","year":"1978"},{"key":"10.1016\/0004-3702(86)90011-1_BIB13","series-title":"Proceedings 3rd AISB\/GI Conference","article-title":"Analyzing and representing natural language in logic","author":"Brown","year":"1978"},{"key":"10.1016\/0004-3702(86)90011-1_BIB14","unstructured":"Brown, F.M. and Schwind, C.B., Towards an integrated theory of natural language understanding, Linguistics J., microfiche."},{"key":"10.1016\/0004-3702(86)90011-1_BIB15","series-title":"Representation and Processing of Natural Language","article-title":"Outline of an integrated theory of natural language understanding","author":"Brown","year":"1980"},{"key":"10.1016\/0004-3702(86)90011-1_BIB16","article-title":"An automatic proof of the completeness of quantificational logic","author":"Brown","year":"1978","journal-title":"Department of Artificial Intelligence Research Rept. 52"},{"key":"10.1016\/0004-3702(86)90011-1_BIB17","series-title":"Proceedings Fourth Conference on Automatic Theorem Proving","article-title":"A theorem prover for metatheory","author":"Brown","year":"1979"},{"key":"10.1016\/0004-3702(86)90011-1_BIB18","article-title":"Logic algorithms for natural numbers","author":"Brown","year":"1979","journal-title":"TR 108"},{"key":"10.1016\/0004-3702(86)90011-1_BIB19","article-title":"A deductive system for meta theoretic reasoning","author":"Brown","year":"1980","journal-title":"TR 132"},{"key":"10.1016\/0004-3702(86)90011-1_BIB20","article-title":"A deductive system for real algebra","author":"Brown","year":"1980","journal-title":"TR 141"},{"key":"10.1016\/0004-3702(86)90011-1_BIB21","article-title":"A sequent calculus for intensional logic","author":"Brown","year":"1980","journal-title":"TR 143"},{"key":"10.1016\/0004-3702(86)90011-1_BIB22","series-title":"Proceedings NSF Workshop on Logic Programming","article-title":"Computation with automatic theorem provers","author":"Brown","year":"1981"},{"key":"10.1016\/0004-3702(86)90011-1_BIB23","series-title":"Proceedings Ninth International Joint Conference on Artificial Intelligence","article-title":"A logic programming and verification system for recursive quantificational logic","author":"Brown","year":"1985"},{"key":"10.1016\/0004-3702(86)90011-1_BIB24","article-title":"Fundamentals of QCL programming system","author":"Brown","year":"1984"},{"key":"10.1016\/0004-3702(86)90011-1_BIB25","doi-asserted-by":"crossref","DOI":"10.1093\/comjnl\/12.1.41","article-title":"Proving properties of programs by structural induction","volume":"12","author":"Burstall","year":"1969","journal-title":"Computer J."},{"key":"10.1016\/0004-3702(86)90011-1_BIB26","series-title":"Proceedings First National Conference on Artificial Intelligence","article-title":"HCPRVR; An interpreter for logic programs","author":"Chester","year":"1980"},{"key":"10.1016\/0004-3702(86)90011-1_BIB27","series-title":"Logic and Data Bases","article-title":"Negation as failure","author":"Clark","year":"1978"},{"key":"10.1016\/0004-3702(86)90011-1_BIB28","series-title":"Proceedings Seventh International Joint Conference on Artificial Intelligence","article-title":"Last steps towards an ultimate Prolog","author":"Colmerauer","year":"1981"},{"key":"10.1016\/0004-3702(86)90011-1_BIB29","series-title":"Proceedings First International Joint Conference on Artificial Intelligence","article-title":"Applications of theorem proving to problem solving","author":"Green","year":"1969"},{"key":"10.1016\/0004-3702(86)90011-1_BIB30","series-title":"From Frege to G\u00f6del","article-title":"Begriffschrift, a formula language, modeled upon that of arithmetic, for pure thought, 1879","author":"Frege","year":"1967"},{"key":"10.1016\/0004-3702(86)90011-1_BIB31","series-title":"Proceedings 2nd MFCS Symposium Czechoslovak Academy of Science","first-page":"105","article-title":"Computation and deduction","author":"Hayes","year":"1973"},{"key":"10.1016\/0004-3702(86)90011-1_BIB32","author":"Henry","year":"1972"},{"key":"10.1016\/0004-3702(86)90011-1_BIB33","series-title":"Proceedings Second International Joint Conference on Artificial Intelligence","article-title":"Procedural embedding of knowledge in planner","author":"Hewitt","year":"1971"},{"key":"10.1016\/0004-3702(86)90011-1_BIB34","series-title":"From Frege to G\u00f6del","article-title":"The foundations of mathematics","author":"Hilbert","year":"1967"},{"key":"10.1016\/0004-3702(86)90011-1_BIB35","article-title":"Some special purpose resolution systems","volume":"7","author":"Kuehner","year":"1972"},{"key":"10.1016\/0004-3702(86)90011-1_BIB36","article-title":"A proof procedure using connection graphs","volume":"22","author":"Kowalski","year":"1974","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(86)90011-1_BIB37","series-title":"Proceedings of the IFIP Congress 74","first-page":"569","article-title":"Predicate logic as programming language","author":"Kowalski","year":"1974"},{"key":"10.1016\/0004-3702(86)90011-1_BIB38","author":"Kowalski","year":"1979"},{"key":"10.1016\/0004-3702(86)90011-1_BIB39","series-title":"Leibniz Philosophical Writings","article-title":"Of universal synthethesis and analysis; or the art of discovery and judgement, 1683","author":"Leibniz","year":"1973"},{"key":"10.1016\/0004-3702(86)90011-1_BIB40","series-title":"Ph.D. thesis","article-title":"A logic based programming system","author":"Liu","year":"1985"},{"key":"10.1016\/0004-3702(86)90011-1_BIB41","author":"Luschei","year":"1962","journal-title":"The Logical Systems of Lesniewski"},{"key":"10.1016\/0004-3702(86)90011-1_BIB42","author":"McCarthy","year":"1966"},{"key":"10.1016\/0004-3702(86)90011-1_BIB43","article-title":"The programming of deduction and induction","author":"Meltzer","year":"1971"},{"key":"10.1016\/0004-3702(86)90011-1_BIB44","first-page":"28","article-title":"The impossibility of perfect proof procedures","volume":"15","author":"Meltzer","year":"1973","journal-title":"AISB European Newsletter"},{"key":"10.1016\/0004-3702(86)90011-1_BIB45","series-title":"MACLISP reference manual","author":"Moon","year":"1974"},{"key":"10.1016\/0004-3702(86)90011-1_BIB46","article-title":"Computational logic: Structure sharing and proof of program properties","author":"Moore","year":"1973"},{"key":"10.1016\/0004-3702(86)90011-1_BIB47","author":"Morse","year":"1965"},{"key":"10.1016\/0004-3702(86)90011-1_BIB48","series-title":"These de 3\u00e8me cycle","article-title":"Demonstration automatique de theorems en theorie des ensembles","author":"Pastre","year":"1976"},{"key":"10.1016\/0004-3702(86)90011-1_BIB49","doi-asserted-by":"crossref","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","article-title":"An improved proof procedure","volume":"26","author":"Prawitz","year":"1960","journal-title":"Theoria"},{"key":"10.1016\/0004-3702(86)90011-1_BIB50","article-title":"The use of models in automatic theorem proving","author":"Reiter","year":"1972"},{"key":"10.1016\/0004-3702(86)90011-1_BIB51","doi-asserted-by":"crossref","DOI":"10.1145\/321250.321253","article-title":"A machine oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(86)90011-1_BIB52","article-title":"Completeness and soundness of the connection graph proof procedure","author":"Siekmann","year":"1978"},{"key":"10.1016\/0004-3702(86)90011-1_BIB53","article-title":"Ein Formalismus zur Beschreibung der Syntax und Bedeutung von Frage-Antwort-Systemen","author":"Schwind","year":"1977"},{"key":"10.1016\/0004-3702(86)90011-1_BIB54","series-title":"From Frege to G\u00f6del","article-title":"The foundations of elementary arithmetic established by the recursive mode of thought, without the use of apparent variables ranging over infinite domains, 1923","author":"Skolem","year":"1961"},{"key":"10.1016\/0004-3702(86)90011-1_BIB55","year":"1969"},{"key":"10.1016\/0004-3702(86)90011-1_BIB56","article-title":"INTERLISP reference manual","author":"Teitelman","year":"1974","journal-title":"XEROX"},{"key":"10.1016\/0004-3702(86)90011-1_BIB57","doi-asserted-by":"crossref","DOI":"10.1147\/rd.41.0002","article-title":"Toward mechanical mathematics","volume":"4","author":"Wang","year":"1960","journal-title":"IBM J. Res. Development"},{"key":"10.1016\/0004-3702(86)90011-1_BIB58","series-title":"Lecture Notes in Mathematics: Symposium on Automatic Demonstration","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0060627","article-title":"On the long-range prospects of automatic theorem-proving","author":"Wang","year":"1970"},{"key":"10.1016\/0004-3702(86)90011-1_BIB59","series-title":"Syntactic trees and connection graphs","author":"Brown","year":"1977"},{"key":"10.1016\/0004-3702(86)90011-1_BIB60","series-title":"Functional and Logic Programming","article-title":"EQLOG: Equality, types, and generic modules for logic programming","author":"Goguen","year":"1985"},{"key":"10.1016\/0004-3702(86)90011-1_BIB61","first-page":"181","article-title":"Search strategies for theorem proving","volume":"5","author":"Kowalski","year":"1969"},{"key":"10.1016\/0004-3702(86)90011-1_BIB62","article-title":"A hole in goal trees: Some guidance from resolution theory","volume":"25","author":"Loveland","year":"1976","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/0004-3702(86)90011-1_BIB63","author":"McClune","year":"1986","journal-title":"Private ARPAnet communication from Argonne National Lab. to J. Siekmann"},{"key":"10.1016\/0004-3702(86)90011-1_BIB64","author":"Quine","year":"1969"},{"key":"10.1016\/0004-3702(86)90011-1_BIB65","article-title":"LOGLISP: An alternative to PROLOG","volume":"10","author":"Robinson","year":"1982"},{"key":"10.1016\/0004-3702(86)90011-1_BIB66","doi-asserted-by":"crossref","DOI":"10.1145\/361002.361016","article-title":"Mechanical program analysis","volume":"18","author":"Wegbreit","year":"1975","journal-title":"Comm. ACM"},{"key":"10.1016\/0004-3702(86)90011-1_BIB67","article-title":"Verifying program performance","volume":"23","author":"Wegbreit","year":"1974","journal-title":"J. ACM"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370286900111?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370286900111?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T09:52:19Z","timestamp":1704793939000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0004370286900111"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986,11]]},"references-count":67,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1986,11]]}},"alternative-id":["0004370286900111"],"URL":"https:\/\/doi.org\/10.1016\/0004-3702(86)90011-1","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1986,11]]}}}