{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:14:46Z","timestamp":1725488086745},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651413"},{"type":"electronic","value":"9783540495451"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49545-2_9","type":"book-chapter","created":{"date-parts":[[2007,8,6]],"date-time":"2007-08-06T14:41:28Z","timestamp":1186411288000},"page":"122-138","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["A Deduction Method Complete for Refutation and Finite Satisfiability"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Bry","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sunna","family":"Torge","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,2,26]]},"reference":[{"key":"9_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027015","volume-title":"Proc. 6th Int. Conf. on Algebraic and Logic Programming","author":"S. Abdennadher","year":"1997","unstructured":"S. Abdennadher and H. Sch\u00fctz. Model Generation with Existentially Quantified Variables and Constraints. Proc. 6th Int. Conf. on Algebraic and Logic Programming, Springer LNCS 1298, 1997."},{"key":"9_CR2","unstructured":"C. Aravindan and P. Baumgartner. A Rational and Efficient Algorithm for View Deletion in Databases. Proc. Int. Logic Programming Symposium, MIT Press, 1997."},{"key":"9_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 5th Europ. Workshop on Logics in AI (JELIA)","author":"P. Baumgartner","year":"1996","unstructured":"P. Baumgartner, U. Furbach, and I. Niemel\u00e4. Hyper tableaux. Proc. 5th Europ. Workshop on Logics in AI (JELIA), Springer LNCS 1126, 1996."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"P. Baumgartner, P. Fr\u00f6hlich, U. Furbach, and W. Nejdl. Tableaux for Diagnosis Applications. Proc. 6th Workshop on Theorem Proving with Tableaux and Related Methods, Springer LNAI, 76\u201390, 1997.","DOI":"10.1007\/BFb0027406"},{"key":"9_CR5","unstructured":"P. Baumgartner, P. Fr\u00f6hlich, U. Furbach, and W. Nejdl. Semantically Guided Theorem Proving for Diagnosis Applications. Proc. 15th Int. Joint Conf. on Artificial Intelligence (IJCAI), 460\u2013465, 1997."},{"key":"9_CR6","unstructured":"E. W. Beth. The Foundations of Mathematics. North Holland, 1959."},{"key":"9_CR7","unstructured":"F. Bry. Intensional Updates: Abduction via Deduction. Proc. 7th Int. Conf. on Logic Programming, MIT Press, 561\u2013575, 1990."},{"key":"9_CR8","unstructured":"F. Bry, N. Eisinger, H. Sch\u00fctz, and S. Torge. SIC: An Interactive Tool for the Design of Integrity Constraints (System Description). EDBT\u201998 Demo Session Proceedings, 45\u201346, 1998."},{"key":"9_CR9","unstructured":"F. Bry, N. Eisinger, H. Sch\u00fctz, and S. Torge. SIC: Satisfiability Checking for Integrity Constraints. Proc. Deductive Databases and Logic Programming (DDLP), Workshop at JICSLP, 1998."},{"key":"9_CR10","series-title":"Lect Notes Comput Sci","first-page":"44","volume-title":"Proc. 1st Workshop on Computer Science Logic","author":"F. Bry","year":"1987","unstructured":"F. Bry and R. Manthey. Proving Finite Satisfiability of Deductive Databases. Proc. 1st Workshop on Computer Science Logic, Springer LNCS 329, 44\u201355, 1987."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"F. Bry and A. Yahya. Minimal Model Generation with Positive Unit Hyperresolution Tableaux. Proc. 5th Workshop on Theorem Proving with Tableaux and Related Methods, Springer LNAI 1071, 1996.","DOI":"10.1007\/3-540-61208-4_10"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1093\/logcom\/3.1.3","volume":"3","author":"R. Caferra","year":"1993","unstructured":"R. Caferra and N. Zabel. Building Models by Using Tableaux Extended by Equational Problems. J. of Logic and Computation, 3, 3\u201325, 1993.","journal-title":"J. of Logic and Computation"},{"issue":"1-2","key":"9_CR13","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(94)90208-9","volume":"122","author":"Marc Denecker","year":"1994","unstructured":"M. Denecker and D. de Schreye. On the Duality of Abduction and Model Generation in a Framework of Model Generation with Equality. Theoretical Computer Science, 122, 1994.","journal-title":"Theoretical Computer Science"},{"key":"9_CR14","unstructured":"N. Eisinger and T. Geisler. Problem Solving with Model-Generation Approaches based on PUHR Tableaux. Proc. Workshop on Problem-solving Methodologies with Automated Deduction, Workshop at CADE-15, 1998."},{"issue":"2","key":"9_CR15","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. Ferm\u00fcller","year":"1996","unstructured":"C. Ferm\u00fcller and A. Leitsch. Hyperresolution and Automated Model Building. J. of Logic and Computation, 6:2, 173\u2013203, 1996.","journal-title":"J. of Logic and Computation"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"9_CR17","unstructured":"H. Fujita and R. Hasegawa. A Model Generation Theorem Prover in KL1 Using a Ramified-Stack Algorithm. Proc. 8th Int. Conf. on Logic Programming, MIT Press, 1991."},{"key":"9_CR18","unstructured":"U. Furbach, ed. Tableaux and Connection Calculi. Part I. In Automated Deduction \u2014 A Basis for Applications. Kluwer Academic Publishers, 1998. To appear."},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/356924.356929","volume":"16","author":"H. Gallaire","year":"1984","unstructured":"H. Gallaire, J. Minker, and J.-M. Nicolas. Logic and Databases: A Deductive Approach. ACM Computing Surveys, 16:2, 1984.","journal-title":"ACM Computing Surveys"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"J. Hintikka. Model Minimization-An Alternative to Circumscription. J. of Automated Reasoning, 4, 1988.","DOI":"10.1007\/BF00244510"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"K. M. H\u00f6rnig. Generating Small Models of First Order Axioms. Proc. GWAI-81, Informatik-Fachberichte 47, Springer-Verlag, 1981.","DOI":"10.1007\/978-3-662-02328-0_23"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"M. Kettner and N. Eisinger. The Tableaux Browser SNARKS (System Description). Proc. 14th Int. Conf. on Automated Deduction, Springer LNAI 1249, 1997.","DOI":"10.1007\/3-540-63104-6_40"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"S. Lorenz. A Tableaux Prover for Domain Minimization. J. of Automated Reasoning, 13, 1994.","DOI":"10.1007\/BF00881950"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00881861","volume":"14","author":"D. W. Loveland","year":"1995","unstructured":"D. W. Loveland, D. W. Reed, and D. S. Wilson. SATCHMORE: SATCHMO with RElevancy. J. of Automated Reasoning, 14, 325\u2013351, 1995.","journal-title":"J. of Automated Reasoning"},{"key":"9_CR25","unstructured":"R. Manthey and F. Bry. SATCHMO: A Theorem Prover Implemented in Prolog. Proc. 9th Int. Conf. on Automated Deduction, Springer LNAI 310, 1988."},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"I. Niemel\u00e4. A Tableaux Calculus for Minimal Model Reasoning. Proc. 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Springer LNAI 1071, 1996.","DOI":"10.1007\/3-540-61208-4_18"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"N. Peltier. Simplifying and Generalizing Formulae in Tableaux. Pruning the Search Space and Building Models. Proc. 6th Workshop on Theorem Proving with Tableaux and Related Methods, Springer LNAI 1227, 1997.","DOI":"10.1007\/BFb0027423"},{"key":"9_CR28","unstructured":"D. Poole. Normality and Faults in Logic-Based Diagnosis. Proc. 11th Int. Joint Conf. on Artificial Intelligence, 1304\u20131310, 1985."},{"key":"9_CR29","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R. Reiter","year":"1987","unstructured":"R. Reiter. A Theory of Diagnosis from First Principles. Artificial Intelligence, 32, 57\u201395, 1987.","journal-title":"Artificial Intelligence"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"M. Paramasivam and D. Plaisted. Automated Deduction Techniques for Classification in Description Logic Systems. J. of Automated Reasoning, 20(3), 1998.","DOI":"10.1023\/A:1005866922570"},{"key":"9_CR31","volume-title":"Finder (finite domain enumerator): Notes and Guides","author":"J. Slaney","year":"1992","unstructured":"J. Slaney. Finder (finite domain enumerator): Notes and Guides. Tech. rep., Australian National University Automated Reasoning Project, Canberra, 1992."},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"R. Smullyan. First-Order Logic. Springer, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"9_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019355","volume-title":"Baltic Computer Science","author":"T. Tammet","year":"1991","unstructured":"T. Tammet. Using Resolution for Deciding Solvable Classes and Building Finite Models. Baltic Computer Science, Springer LNCS 502, 1991."},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"G. Wrightson. ed. Special Issue on Automated Reasoning with Analytic Tableaux, Parts I and II. J. of Automated Reasoning, 13:2 and 3, 173\u2013421, 1994.","DOI":"10.1007\/BF00881953"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"M. Tiomkin. Proving Unprovability. Proc. 3rd Symp. Logic in Computer Science, 22\u201326, 1988.","DOI":"10.1109\/LICS.1988.5097"},{"key":"9_CR36","unstructured":"B. A. Trakhtenbrot. Impossibility of an Algorithm for the Decision Problem in Finite Classes. Proc. Dokl. Acad. Nauk., SSSR 70, 1950."},{"key":"9_CR37","unstructured":"Jian Zhang and Hantao Zhang. SEM: A System for Enumerating Models. Proc. International Joint Conference on Artificial Intelligence, 1995"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49545-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T10:01:03Z","timestamp":1558260063000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49545-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651413","9783540495451"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-49545-2_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"26 February 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}