{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T21:40:03Z","timestamp":1706650803207},"reference-count":22,"publisher":"Duke University Press","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Notre Dame J. Formal Logic"],"published-print":{"date-parts":[[1995,7,1]]},"DOI":"10.1305\/ndjfl\/1040149359","type":"journal-article","created":{"date-parts":[[2003,2,25]],"date-time":"2003-02-25T21:26:39Z","timestamp":1046208399000},"source":"Crossref","is-referenced-by-count":1,"title":["A Finitely Axiomatized Formalization of Predicate Calculus with Equality"],"prefix":"10.1215","volume":"36","author":[{"given":"Norman D.","family":"Megill","sequence":"first","affiliation":[]}],"member":"73","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"Boyer, R., E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos, \u201cSet theory in first order logic: clauses for G\u00f6del's axioms,\u201d <i>Journal of Automated Reasoning<\/i>, vol. 2 (1986), pp. 287\u2013327. Zbl 0635.03008","DOI":"10.1007\/BF02328452"},{"key":"2","unstructured":"Church, A., <i>Introduction to Mathematical Logic<\/i>, Volume 1, Princeton University Press, Princeton, 1956. Zbl 0073.24301 MR 18,631a"},{"key":"3","unstructured":"Cohen, P. J., <i>Set Theory and the Continuum Hypothesis<\/i>, W. A. Benjamin, Reading, 1966. Zbl 0182.01301 MR 38:999"},{"key":"4","unstructured":"Hamilton, A. G., <i>Logic for Mathematicians<\/i>, Cambridge University Press, Cambridge, 1988. Zbl 0653.03001 MR 89e:03002"},{"key":"5","doi-asserted-by":"publisher","unstructured":"Hindley, J. R., and D. Meredith, \u201cPrincipal type-schemes and condensed detachment,\u201d <i>The Journal of Symbolic Logic<\/i>, vol. 55 (1990), pp. 90\u2013105. Zbl 0708.03007 MR 91b:03020","DOI":"10.2307\/2274956"},{"key":"6","doi-asserted-by":"publisher","unstructured":"Kalish, D., and R. Montague, \u201cOn Tarski's formalization of predicate logic with identity,\u201d <i> Archiv f\u00fcr Mathematische Logik und Grundlagenforschung<\/i>, vol. 7 (1965), pp. 81\u2013101. Zbl 0166.00105 MR 34:2438","DOI":"10.1007\/BF01969434"},{"key":"7","doi-asserted-by":"crossref","unstructured":"Kalman, J. A., \u201cCondensed detachment as a rule of inference,\u201d <i>Studia Logica<\/i>, vol. 42 (1983), pp. 443\u2013451. Zbl 0568.03010 MR 86g:03016","DOI":"10.1007\/BF01371632"},{"key":"8","unstructured":"Kleene, S. C., <i>Introduction to Metamathematics<\/i>, Van Nostrand, Princeton, 1952. Zbl 0047.00703 MR 14,525m"},{"key":"9","unstructured":"Megill, N. D., and M. W. Bunder, \u201cWeaker D-complete logics,\u201d The University of Wollongong Department of Mathematics Preprint Series no. 15\/94. Zbl 0845.03010"},{"key":"10","unstructured":"Mendelson, E., <i>Introduction to Mathematical Logic<\/i>, second edition, Van Nostrand, New York, 1979. Zbl 0498.03001 MR 80d:03001"},{"key":"11","doi-asserted-by":"crossref","unstructured":"Meredith, D., \u201cIn memoriam Carew Arthur Meredith (1904\u20131976),\u201d <i> Notre Dame Journal of Formal Logic<\/i>, vol. 18 (1977), pp. 513\u2013516. Zbl 0357.01045 MR 58:10195","DOI":"10.1305\/ndjfl\/1093888116"},{"key":"12","doi-asserted-by":"crossref","unstructured":"Mints, G., and T. Tammet, \u201cCondensed detachment is complete for relevance logic: a computer-aided proof,\u201d <i>Journal of Automated Reasoning<\/i>, vol. 7 (1991), pp. 587\u2013596. Zbl 0751.03011 MR 92h:03028","DOI":"10.1007\/BF01880330"},{"key":"13","doi-asserted-by":"crossref","unstructured":"Monk, J. D., \u201cSubstitutionless predicate logic with identity,\u201d <i> Archiv f\u00fcr Mathematische Logik und Grundlagenforschung<\/i>, vol. 7 (1965), pp. 103\u2013121. Zbl 0158.24603 MR 34:4111","DOI":"10.1007\/BF01969435"},{"key":"14","doi-asserted-by":"crossref","unstructured":"Nemeti, I., \u201cAlgebraizations of quantifier logics, an overview,\u201d version 11.4, preprint, Mathematical Institute, Budapest, 1994. A shortened version without proofs appeared in <i>Studia Logica<\/i>, vol. 50 (1991), pp. 485\u2013569. MR 93h:03082","DOI":"10.1007\/BF00370684"},{"key":"15","doi-asserted-by":"crossref","unstructured":"Peterson, J. G., \u201cAn automatic theorem prover for substitution and detachment systems,\u201d <i>Notre Dame Journal of Formal Logic<\/i>, vol. 19 (1978), pp. 119\u2013122. Zbl 0368.68086 MR 58:8552","DOI":"10.1305\/ndjfl\/1093888213"},{"key":"16","doi-asserted-by":"crossref","unstructured":"Robinson, J. A., \u201cA machine-oriented logic based on the resolution principle,\u201d <i>Journal of the Association for Computing Machinery<\/i>, vol. 12 (1965), pp. 23\u201341. Zbl 0139.12303 MR 30:732","DOI":"10.1145\/321250.321253"},{"key":"17","doi-asserted-by":"crossref","unstructured":"Tarski, A., \u201cA simplified formalization of predicate logic with identity,\u201d <i>Archiv f\u00fcr Mathematische Logik und Grundlagenforschung<\/i>, vol. 7 (1965), pp. 61\u201379. Zbl 0166.00104 MR 34:2437","DOI":"10.1007\/BF01972461"},{"key":"18","doi-asserted-by":"crossref","unstructured":"Tarski, A., and S. Givant, <i>A Formalization of Set Theory Without Variables<\/i>, American Mathematical Society Colloquium Publications, vol. 41, American Mathematical Society, Providence, 1987. Zbl 0654.03036 MR 89g:03012","DOI":"10.1090\/coll\/041"},{"key":"19","unstructured":"Wos, L., <i>Automated Reasoning: 33 Basic Research Problems<\/i>, Prentice-Hall, Englewood Cliffs, 1987 Zbl 0663.68102"},{"key":"20","unstructured":"Wos, L., R. Overbeek, E. Lusk and J. Boyle, <i>Automated Reasoning: Introduction and Applications<\/i>, second edition, McGraw-Hill, New York, 1992. Zbl 0820.68116 MR 93a:68129"},{"key":"21","doi-asserted-by":"crossref","unstructured":"Wos, L. T., and G. A. Robinson, \u201cMaximal models and refutation completeness: semidecision procedures in automated theorem proving,\u201d pp. 609\u2013639 in <i>Word Problems: Decision Problems and the Burnside Problem in Group Theory<\/i>, Studies in Logic and the Foundations of Mathematics, vol. 71, edited by W. W. Boone, F. B. Cannonito, and R. C. Lyndon, North-Holland, Amsterdam, 1973. Zbl 0283.68058 MR 53:7154","DOI":"10.1016\/S0049-237X(08)71923-2"},{"key":"22","unstructured":"Zeman, J. J., <i>Modal Logic<\/i>, Oxford University Press, Oxford, 1973. Zbl 0255.02014 MR 53:2638"}],"container-title":["Notre Dame Journal of Formal Logic"],"original-title":[],"link":[{"URL":"https:\/\/projecteuclid.org\/journalArticle\/Download?urlid=10.1305\/ndjfl\/1040149359","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T21:12:35Z","timestamp":1706649155000},"score":1,"resource":{"primary":{"URL":"https:\/\/projecteuclid.org\/journals\/notre-dame-journal-of-formal-logic\/volume-36\/issue-3\/A-Finitely-Axiomatized-Formalization-of-Predicate-Calculus-with-Equality\/10.1305\/ndjfl\/1040149359.full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,7,1]]},"references-count":22,"journal-issue":{"issue":"3","published-online":{"date-parts":[[1995,7,1]]}},"URL":"https:\/\/doi.org\/10.1305\/ndjfl\/1040149359","relation":{},"ISSN":["0029-4527"],"issn-type":[{"value":"0029-4527","type":"print"}],"subject":[],"published":{"date-parts":[[1995,7,1]]}}}