{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:17Z","timestamp":1725533837109},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026133"},{"type":"electronic","value":"9783642026140"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02614-0_9","type":"book-chapter","created":{"date-parts":[[2009,7,2]],"date-time":"2009-07-02T11:47:24Z","timestamp":1246535244000},"page":"45-58","source":"Crossref","is-referenced-by-count":2,"title":["Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations"],"prefix":"10.1007","author":[{"given":"Gonzalo A.","family":"Aranda-Corral","sequence":"first","affiliation":[]},{"given":"Joaqu\u00edn","family":"Borrego-D\u00edaz","sequence":"additional","affiliation":[]},{"given":"M. Magdalena","family":"Fern\u00e1ndez-Lebr\u00f3n","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-74591-4_11","volume-title":"Theorem Proving in Higher Order Logics","author":"J.-A. Alonso","year":"2007","unstructured":"Alonso, J.-A., Borrego-D\u00edaz, J., Hidalgo, M.-J., Mart\u00edn-Mateos, F.-J., Ruiz-Reina, J.-L.: A Formally Verified Prover for the ALC Description Logic. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 135\u2013150. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"9_CR2","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.artint.2004.11.004","volume":"162","author":"E. Amir","year":"2005","unstructured":"Amir, E., McIlraith, S.: Partition-based logical reasoning for first-order and propositional theories. Artificial Intelligence\u00a0162(1-2), 49\u201388 (2005)","journal-title":"Artificial Intelligence"},{"key":"9_CR3","volume-title":"The Description Logics Handbook. Theory, Implementations and Applications","author":"F. Baader","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinnes, D.L., Nardi, P., Patel-Schneider, P.F.: The Description Logics Handbook. Theory, Implementations and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"9_CR4","first-page":"19","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: A theory of resolution. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, pp. 19\u201399. Elsevier Science Pub., Amsterdam (1998)"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1112\/plms\/s3-73.1.1","volume":"73","author":"P. Beame","year":"1996","unstructured":"Beame, P., Impagliazzo, R., Kraj\u00edcek, J., Pitassi, T., Pudl\u00e1k, P.: Lower Bounds on Hilvert\u2019s Nullstellensatz and propositional proofs. Proc. of London Mathematical Society\u00a073, 1\u201326 (1996)","journal-title":"Proc. of London Mathematical Society"},{"key":"9_CR6","first-page":"107","volume-title":"Proc 3rd Int. Conf. Formal Ontology in Information Systems (FOIS 2004)","author":"B. Bennett","year":"2004","unstructured":"Bennett, B.: Relative Definability in Formal Ontologies. In: Proc 3rd Int. Conf. Formal Ontology in Information Systems (FOIS 2004), pp. 107\u2013118. IOS Press, Amsterdam (2004)"},{"key":"9_CR7","volume-title":"Bin\u00e4re dynamishe systeme","author":"D. Bochmann","year":"1981","unstructured":"Bochmann, D., Posthoff, C.: Bin\u00e4re dynamishe systeme. Akademieverlag, Berlin (1981)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/11556985_33","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST 2005","author":"J. Borrego-D\u00edaz","year":"2005","unstructured":"Borrego-D\u00edaz, J., Ch\u00e1vez-Gonz\u00e1lez, A.M.: Extension of ontologies assisted by automated reasoning systems. In: Moreno D\u00edaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2005. LNCS, vol.\u00a03643, pp. 247\u2013253. Springer, Heidelberg (2005)"},{"key":"9_CR9","unstructured":"Borrego-D\u00edaz, J., Ch\u00e1vez-Gonz\u00e1lez, A.M.: Controlling ontology extension by uncertain concepts through cognitive entropy. In: Proc. Workshop ISWC05 Uncertainty Reasoning on the Semantic Web URSW 2005, pp. 56\u201366 (2005), http:\/\/ftp.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s00037-002-0171-6","volume":"11","author":"J. Buresh-Oppenheim","year":"2003","unstructured":"Buresh-Oppenheim, J., Clegg, M., Imppagliazzo, R., Pitassi, T.: Homogeneization and the Polynomial Calculus. Computational Complexity\u00a011, 91\u2013108 (2003)","journal-title":"Computational Complexity"},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/s10817-007-9078-x","volume":"39","author":"D. Calvanese","year":"2007","unstructured":"Calvanese, D., De Giacomo, G., Lombo, D., Lenserini, M., Rosati, R.: Tractable Reasoning and Efficient Query Answering in Description Logics: The DL\u2009\u2212\u2009Lite Family. J. Automated Reasoning\u00a039, 385\u2013429 (2007)","journal-title":"J. Automated Reasoning"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/S0747-7171(08)80043-0","volume":"11","author":"J. Chazarain","year":"1991","unstructured":"Chazarain, J., Alonso-Jim\u00e9nez, J.A., Briales-Morales, E., Riscos-Fern\u00e1ndez, A.: Multi-valued logic and Gr\u00f6bner bases with applications to modal logic. Journal Symbolic Computation\u00a011, 181\u2013194 (1991)","journal-title":"Journal Symbolic Computation"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Clegg, M., Edmonds, J., Impagliazzo, R.: Using Gr\u00f6bner Basis algorithm to find proofs of unsatisfiability. In: Proc. ACM Symposium of Computing, pp. 174\u2013183 (1996)","DOI":"10.1145\/237814.237860"},{"key":"9_CR14","volume-title":"Ideals, Varieties and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra","author":"D. Cox","year":"2005","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer, Heidelberg (2005)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Cuenca-Grau, B., Parsia, B., Sirin, E., Kalyanpur, A.: Automatic Partitioning of OWL Ontologies Using E-Connections. In: Proc. 2005 Int. Workshop on Description Logics (DL2005) (2005), http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/Vol-147\/21-Grau.pdf","DOI":"10.2139\/ssrn.3199326"},{"key":"9_CR16","first-page":"1","volume":"9","author":"F. Giunchiglia","year":"2007","unstructured":"Giunchiglia, F., Yatskevitch, M., Shvaiko, P.: Semantic Matching: Algorithms and Implementations. J. Data Semantics\u00a09, 1\u201338 (2007)","journal-title":"J. Data Semantics"},{"issue":"1","key":"9_CR17","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/S0021-8693(03)00238-2","volume":"265","author":"M. Fern\u00e1ndez-Lebr\u00f3n","year":"2003","unstructured":"Fern\u00e1ndez-Lebr\u00f3n, M., Narv\u00e1ez-Macarro, L.: Hasse-Schmidt Derivations and Coefficient Fields in Positive Characteristics. J. of Algebra\u00a0265(1), 200\u2013210 (2003)","journal-title":"J. of Algebra"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Kapur, D., Narendran, P.: An equational approach to theorem proving in first-order predicate calculus. In: Proc. 9 Int. Joint Conf. on Artificial Intelligence (IJCAI 1985), pp. 1146\u20131153 (1985)","DOI":"10.1145\/1012497.1012521"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s005000050086","volume":"3","author":"L.M. Laita","year":"1999","unstructured":"Laita, L.M., Roanes-Lozano, E., de Ledesma, L., Alonso-Jim\u00e9nez, J.A.: A computer algebra approach to verification and deduction in many-valued knowledge systems. Soft Computing\u00a03, 7\u201319 (1999)","journal-title":"Soft Computing"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-73595-3_7","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Lutz","year":"2007","unstructured":"Lutz, C., Wolter, F.: Conservative extensions in the lightweight description logic EL. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 84\u201399. Springer, Heidelberg (2007)"},{"issue":"4","key":"9_CR21","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF03177742","volume":"32","author":"F.J. Mart\u00edn-Mateos","year":"2004","unstructured":"Mart\u00edn-Mateos, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz-Reina, J.L.: Formal Verification of a Generic Framework to Synthetize SAT-Provers. J Aut. Reasoning\u00a032(4), 287\u2013313 (2004)","journal-title":"J Aut. Reasoning"},{"key":"9_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10286-8","volume-title":"Boolean Calculus of Differences","author":"A. Thayse","year":"1981","unstructured":"Thayse, A.: Boolean Calculus of Differences. Springer, Berlin (1981)"},{"key":"9_CR23","unstructured":"Tsarkov, D., Horrocks, I.: Optimised Classification for Taxonomic Knowledge Bases. In: Proc. 2005 Int. Workshop on Description Logics (DL 2005) (2005), http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/Vol-147\/39-TsarHorr.pdf"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02614-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T05:39:04Z","timestamp":1589953144000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02614-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026133","9783642026140"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02614-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}