{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:38:22Z","timestamp":1753889902813,"version":"3.41.2"},"reference-count":29,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T00:00:00Z","timestamp":1330992000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"Austrian Science Fund","award":["Y 544"],"award-info":[{"award-number":["Y 544"]}]},{"name":"Austrian Science Fund","award":["P 22416"],"award-info":[{"award-number":["P 22416"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>G\\\"odel logic with the projection operator Delta (G_Delta) is an important many-valued as well as intermediate logic. In contrast to classical logic, the validity and the satisfiability problems of G_Delta are not directly dual to each other. We nevertheless provide a uniform, computational treatment of both problems for prenex formulas by describing appropriate translations into sets of order clauses that can be subjected to chaining resolution. For validity a version of Herbrand's Theorem allows us to show the soundness of standard Skolemization. For satisfiability the translation involves a novel, extended Skolemization method.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:20)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":2,"title":["Theorem proving for prenex G\\\"odel logic with Delta: checking validity and unsatisfiability"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7815-2501","authenticated-orcid":false,"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6947-8772","authenticated-orcid":false,"given":"Agata","family":"Ciabattoni","sequence":"additional","affiliation":[]},{"given":"Christian G","family":"Ferm\u00fcller","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,6]]},"reference":[{"key":"10.2168\/LMCS-8(1:20)2012_avr91","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531058"},{"key":"10.2168\/LMCS-8(1:20)2012_baaz96","doi-asserted-by":"crossref","unstructured":"M. Baaz. Infinite-valued G\u00f6del logics with 0-1-projections and relativizations. InProceedings G\u00f6del 96. Kurt G\u00f6del's Legacy. Springer LNL 6, 23-33, 1996.","DOI":"10.1007\/978-3-662-21963-8_2"},{"key":"10.2168\/LMCS-8(1:20)2012_BCF01","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Ciabattoni and C.G. Ferm\u00fcller. Herbrand's Theorem for prenex G\u00f6del logic and its consequences for theorem proving.Proceedings of LPAR'2001. Springer LNAI 2250, 201-216, 2001.","DOI":"10.1007\/3-540-45653-8_14"},{"key":"10.2168\/LMCS-8(1:20)2012_BCF03","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.6.835"},{"key":"10.2168\/LMCS-8(1:20)2012_BCP09","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Ciabattoni and N. Preining. SAT in monadic G\u00f6del logics: a borderline between decidability and undecidability.Proceedings of WOLLIC 2009. Springer LNAI 5514, 113-123, 2009.","DOI":"10.1007\/978-3-642-02261-6_10"},{"key":"10.2168\/LMCS-8(1:20)2012_BHW","unstructured":"M. Baaz, S. Hetzl and D. Weller. On the complexity of proof deskolemization.J. Symbolic Logic. To appear."},{"key":"10.2168\/LMCS-8(1:20)2012_Handbook","doi-asserted-by":"crossref","unstructured":"M. Baaz, U. Egly and A. Leitsch. Normal form transformations.Handbook of Automated Reasoning, Vol. 1. Eds: A. Robinson, A. Voronkov. Elsevier, 2001, 273-333.","DOI":"10.1016\/B978-044450813-3\/50007-2"},{"key":"10.2168\/LMCS-8(1:20)2012_BF10","doi-asserted-by":"crossref","unstructured":"M. Baaz and C.G. Ferm\u00fcller. A resolution mechanism for prenex G\u00f6del logic. InProceedings of CSL 2010. Springer LNCS 6247, 67-79, 2010.","DOI":"10.1007\/978-3-642-15205-4_9"},{"key":"10.2168\/LMCS-8(1:20)2012_HBMFL_goedel","unstructured":"M. Baaz and N. Preining. G\u00f6del-Dummett logics.Handbook of Mathematical Fuzzy Logic, volume 2, Eds: P. Cintula, P. H\u00e1jek, C. Noguera. College Publications, pp. 585-627, 2011."},{"key":"10.2168\/LMCS-8(1:20)2012_BPZ07","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.apal.2007.03.001","volume":"147","author":"M. Baaz, N. Preining and R. Zach","year":"2007","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-8(1:20)2012_BGcade","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Ordered chaining for total orderings.Proc. CADE`94, Springer LNCS 814, 1994, 435-450.","DOI":"10.1007\/3-540-58156-1_32"},{"key":"10.2168\/LMCS-8(1:20)2012_BGjacm","doi-asserted-by":"publisher","DOI":"10.1145\/293347.293352"},{"key":"10.2168\/LMCS-8(1:20)2012_CR10","unstructured":"A. Ciabattoni and P. Rusnok. On the classical content of monadic Gsimand its application to a fuzzy medical expert system,Proceedings of KR 2010, AAAI, 373-381, 2010."},{"key":"10.2168\/LMCS-8(1:20)2012_DV","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Decidability problems for the prenex fragment of intuitionistic logic. InProceedings LICS'96. IEEE Press, 503-509, 1996.","DOI":"10.1109\/LICS.1996.561467"},{"key":"10.2168\/LMCS-8(1:20)2012_dummett","doi-asserted-by":"publisher","DOI":"10.2307\/2964753"},{"key":"10.2168\/LMCS-8(1:20)2012_Gab72","doi-asserted-by":"publisher","DOI":"10.2307\/2272747"},{"key":"10.2168\/LMCS-8(1:20)2012_Fiorino","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2010.06.004"},{"key":"10.2168\/LMCS-8(1:20)2012_hajek","doi-asserted-by":"crossref","unstructured":"P. Hajek.Metamathematics of Fuzzy Logic. Kluwer, 1998.","DOI":"10.1007\/978-94-011-5300-3"},{"key":"10.2168\/LMCS-8(1:20)2012_hajek1","doi-asserted-by":"crossref","unstructured":"P. Hajek. Arithmetical complexity of fuzzy predicate logics - a survey.Soft Computing9\/12: 935-941, 2005.","DOI":"10.1007\/s00500-004-0448-6"},{"key":"10.2168\/LMCS-8(1:20)2012_hajek2","doi-asserted-by":"crossref","unstructured":"P. Hajek. Arithmetical complexity of fuzzy predicate logics - a survey II.Annals of Pure and Applied Logic161(2): 212-219, 2009.","DOI":"10.1016\/j.apal.2009.05.015"},{"key":"10.2168\/LMCS-8(1:20)2012_HB","unstructured":"D. Hilbert and P. Bernays.Grundlagen der Mathematik, Vol. 2, Berlin: Springer 1939."},{"key":"10.2168\/LMCS-8(1:20)2012_LW07","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9047-9"},{"key":"10.2168\/LMCS-8(1:20)2012_leitsch","doi-asserted-by":"crossref","unstructured":"A. Leitsch.The Resolution Calculus. Springer (fomerly Kluwer) 1997.","DOI":"10.1007\/978-3-642-60605-2"},{"key":"10.2168\/LMCS-8(1:20)2012_LPV","doi-asserted-by":"publisher","DOI":"10.1145\/383779.383783"},{"key":"10.2168\/LMCS-8(1:20)2012_Mint","unstructured":"G. Mints. The Skolem method in intuitionistic calculi.Proceedings of Steklov Institute of Mathematics, 121: 73-109, 1972."},{"key":"10.2168\/LMCS-8(1:20)2012_PG","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"10.2168\/LMCS-8(1:20)2012_P10","doi-asserted-by":"crossref","unstructured":"N. Preining. G\u00f6del logics - a survey.Proceedings of LPAR 2010. Springer LNCS 6397, pp. 30-51, 2010.","DOI":"10.1007\/978-3-642-16242-8_4"},{"key":"10.2168\/LMCS-8(1:20)2012_TT84","doi-asserted-by":"publisher","DOI":"10.2307\/2274139"},{"key":"10.2168\/LMCS-8(1:20)2012_visser","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(82)90024-9"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/833\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/833\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:09:41Z","timestamp":1744067381000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/833"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,6]]},"references-count":29,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:20)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1202.6352","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1202.6352","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,3,6]]},"article-number":"833"}}