{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:16:56Z","timestamp":1725560216428},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_30","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T14:56:52Z","timestamp":1279724212000},"page":"409-423","source":"Crossref","is-referenced-by-count":7,"title":["Model Representation via Contexts and Implicit Generalizations"],"prefix":"10.1007","author":[{"given":"Christian G.","family":"Ferm\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhard","family":"Pichler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","volume-title":"Proceedings of ESFOR 2004","author":"P. Baumgartner","year":"2004","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Darwin: A theorem prover for the model evolution calculus. In: Proceedings of ESFOR 2004, Elsevier, Amsterdam (2004)"},{"issue":"3","key":"30_CR2","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1023\/B:JARS.0000044872.51237.c9","volume":"32","author":"P. Baumgartner","year":"2004","unstructured":"Baumgartner, P., Furbach, U., Gross-Hardt, M., Sinner, A.: Living Book \u2013 Deduction, Slicing, and Interaction. Journal of Automated Reasoning\u00a032(3), 259\u2013286 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Gross-Hardt, M., Sinner, A.: Living Book \u2013 Deduction, Slicing, and Interaction. Fachberichte Informatik, Universit\u00e4t Koblenz Landau, vol.\u00a02 (2003)","DOI":"10.1007\/978-3-540-45085-6_23"},{"key":"30_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus. Fachberichte Informatik, Universit\u00e4t Koblenz Landau. vol.1 (2003) In: Extended Version of [4] (2003)","DOI":"10.1007\/978-3-540-45085-6_32"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-61208-4_8","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The disconnection method \u2013 a confluent integration of unification in the analytic framework. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/BFb0012853","volume-title":"9th International Conference on Automated Deduction","author":"H.-J. B\u00fcrckert","year":"1988","unstructured":"B\u00fcrckert, H.-J.: Solving disequations in equational theories. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 517\u2013526. Springer, Heidelberg (1988)"},{"key":"30_CR8","volume-title":"Applied Logic Series","author":"R. Caferra","year":"2004","unstructured":"Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. In: Applied Logic Series, vol.\u00a031, Kluwer Academic Publishers, Dordrecht (2004)"},{"key":"30_CR9","unstructured":"Caferra, R., Peltier, N.: Extending semantic resolution via automated model building: applications. In: Proceedings of IJCAI 1995, pp. 328\u2013334 (1995)"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0018439","volume-title":"Logics in AI","author":"R. Caferra","year":"1991","unstructured":"Caferra, R., Zabel, N.: Extending resolution for model construction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol.\u00a0478, pp. 153\u2013169. Springer, Heidelberg (1991)"},{"key":"30_CR11","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"H. Comon","year":"1991","unstructured":"Comon, H.: Disunification: a survey. In: Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge (1991)"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","first-page":"290","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"T. Eiter","year":"1997","unstructured":"Eiter, T., Gottlob, G., Veith, H.: Modular logic programming and generalized quantifiers. In: Fuhrbach, U., Dix, J., Nerode, A. (eds.) LPNMR 1997. LNCS, vol.\u00a01265, pp. 290\u2013309. Springer, Heidelberg (1997)"},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-56992-8_10","volume-title":"Proceedings of CSL 1992","author":"C.G. Ferm\u00fcller","year":"1993","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Model building by resolution. In: Proceedings of CSL 1992. LNCS, vol.\u00a0702, pp. 134\u2013148. Springer, Heidelberg (1993)"},{"issue":"2","key":"30_CR14","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C.G. Ferm\u00fcller","year":"1996","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Hyperresolution and automated model building. Journal of Logic and Computation\u00a06(2), 173\u2013203 (1996)","journal-title":"Journal of Logic and Computation"},{"key":"30_CR15","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.2000.2915","volume":"165","author":"G. Gottlob","year":"2001","unstructured":"Gottlob, G., Pichler, R.: Working with ARMs: Complexity results on atomic representations of Herbrand models. Information and Computation\u00a0165, 183\u2013207 (2001)","journal-title":"Information and Computation"},{"issue":"1&2","key":"30_CR16","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0304-3975(95)00207-3","volume":"166","author":"G. Gottlob","year":"1996","unstructured":"Gottlob, G., Marcus, S., Nerode, A., Salzer, G., Subrahmanian, V.S.: A non-ground realization of the stable and well-founded semantics. Theoretical Computer Science\u00a0166(1&2), 221\u2013262 (1996)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"30_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","volume":"82","author":"J.-P. Jouannaud","year":"1989","unstructured":"Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in theories without constructors. Information and Computation\u00a082(1), 1\u201333 (1989)","journal-title":"Information and Computation"},{"issue":"4","key":"30_CR18","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF01893885","volume":"28","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Rosenkrantz, D., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica\u00a028(4), 311\u2013350 (1991)","journal-title":"Acta Informatica"},{"key":"30_CR19","first-page":"219","volume-title":"Proceedings of ICLP 1987","author":"K. Kunen","year":"1987","unstructured":"Kunen, K.: Answer sets and negation as failure. In: Proceedings of ICLP 1987, pp. 219\u2013228. MIT Press, Cambridge (1987)"},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Mathematical Foundations of Computer Science 1991","author":"J.-L. Lassez","year":"1991","unstructured":"Lassez, J.-L., Maher, M., Marriott, K.: Elimination of negation in term algebras. In: Tarlecki, A. (ed.) MFCS 1991. LNCS, vol.\u00a0520, pp. 1\u201316. Springer, Heidelberg (1991)"},{"issue":"3","key":"30_CR21","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/BF00243794","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. Journal of Automated Reasoning\u00a03(3), 301\u2013317 (1987)","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Letz, R., Stenz, G.: Model Elimination and Connection Tableau Procedures. In: Handbook of Automated Reasoning, June 2001, vol.\u00a0II, pp. 2015\u20132114 (2001)","DOI":"10.1016\/B978-044450813-3\/50030-8"},{"key":"30_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-45653-8_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and model generation with disconnection tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 142\u2013156. Springer, Heidelberg (2001)"},{"key":"30_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-540-25984-8_20","volume-title":"Automated Reasoning","author":"R. Letz","year":"2004","unstructured":"Letz, R., Stenz, G.: Generalised handling of variables in disconnection tableaux. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 289\u2013306. Springer, Heidelberg (2004)"},{"key":"30_CR25","first-page":"348","volume-title":"Proceedings of LICS 1988","author":"M. Maher","year":"1988","unstructured":"Maher, M.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proceedings of LICS 1988, pp. 348\u2013357. IEEE Computer Society, Los Alamitos (1988)"},{"issue":"2","key":"30_CR26","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01534454","volume":"15","author":"M. Maher","year":"1995","unstructured":"Maher, M., Stuckey, P.: On inductive inference of cyclic structures. Annals of Mathematics and Artificial Intelligence\u00a015(2), 167\u2013208 (1995)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"30_CR27","unstructured":"Marriott, K.: Finding Explicit Representations for Subsets of the Herbrand Universe. PhD thesis, University of Melbourne, Australia (1988)"},{"issue":"2","key":"30_CR28","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Transactions on Programming Languages and Systems\u00a04(2), 258\u2013282 (1982)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"30_CR29","unstructured":"Matzinger, R.: Computational representations of models in first-order logic. Technische Universit\u00e4t Wien, Dissertation, Ph.D. thesis (2000)"},{"issue":"1","key":"30_CR30","doi-asserted-by":"publisher","first-page":"1021","DOI":"10.1016\/S0304-3975(02)00583-2","volume":"290","author":"R. Pichler","year":"2003","unstructured":"Pichler, R.: Explicit versus implicit representations of subsets of the Herbrand universe. Theoretical Computer Science\u00a0290(1), 1021\u20131056 (2003)","journal-title":"Theoretical Computer Science"},{"key":"30_CR31","series-title":"LNAI","first-page":"316","volume-title":"Proceedings of CADE-13","author":"S. Vorobyov","year":"1996","unstructured":"Vorobyov, S.: An improved lower bound for the elementary theories of trees. In: Proceedings of CADE-13. LNCS (LNAI), vol.\u00a0690, pp. 316\u2013327. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:09:13Z","timestamp":1605625753000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11532231_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}