{"entities":{"Q1412856":{"pageid":1423596,"ns":120,"title":"Item:Q1412856","lastrevid":71145513,"modified":"2026-04-13T19:46:50Z","type":"item","id":"Q1412856","labels":{"en":{"language":"en","value":"Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2010262"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1412856$7FD0D37B-D3F1-46BE-BBDD-F9E5D46FFD26","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"01974811b3539ae6147cada14a674511361a8702","datavalue":{"value":{"text":"Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1412856$6FB6B045-408B-437C-87D4-550AB34E840D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0111594ed35b3e37daddb2b45069ce57b8df88d0","datavalue":{"value":"1026.00022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$AF9540F3-B721-4CCE-8BC5-24E175249270","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1412856$3FC20D22-0EB4-449E-AB71-40CD062A1505","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d6113ffffcef3e8747b6170d608189aaf7da06e6","datavalue":{"value":{"time":"+2003-11-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1412856$BCEEC518-23C1-4F3C-A76E-70892F271CD7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e6816678650395bd249c0c7e7ebc2af84826f4bc","datavalue":{"value":"http://link.springer.de/link/service/series/0558/tocs/t2741.htm","type":"string"},"datatype":"url"},"type":"statement","id":"Q1412856$F8B68253-88CA-4F08-BD5E-8AC0197614EF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f6cfed3c2ab594d61d75273b0fed5d30e1cf0a1b","datavalue":{"value":"The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 0993.00050).  Indexed articles:  \\textit{Meseguer, Jos\u00e9; Palomino, Miguel; Mart\u00ed-Oliet, Narciso}, Equational abstractions., 2-16 [Zbl 1278.68185]  \\textit{Giesl, J\u00fcrgen; Kapur, Deepak}, Deciding inductive validity of equations., 17-31 [Zbl 1278.68262]  \\textit{Hirokawa, Nao; Middeldorp, Aart}, Automating the dependency pair method., 32-46 [Zbl 1278.68264]  \\textit{Korovin, Konstantin; Voronkov, Andrei}, An AC-compatible Knuth-Bendix order., 47-59 [Zbl 1278.68268]  \\textit{Lutz, Carsten; Sattler, Ulrike; Tendera, Lidia}, The complexity of finite model reasoning in description logics., 60-74 [Zbl 1278.68288]  \\textit{Pan, Guoqiang; Vardi, Moshe Y.}, Optimizing a BDD-based modal solver., 75-89 [Zbl 1278.68277]  \\textit{Hladik, Jan; Sattler, Ulrike}, A translation of looping alternating automata into description logics., 90-105 [Zbl 1278.68265]  \\textit{Crary, Karl; Sarkar, Susmit}, Foundational certified code in a metalogical framework., 106-120 [Zbl 1278.68255]  \\textit{Mehta, Farhad; Nipkow, Tobias}, Proving pointer programs in higher-order logic., 121-135 [Zbl 1278.68274]  \\textit{Hendriks, Dimitri; van Oostrom, Vincent}, \\(\\rightthreetimes\\), 136-150 [Zbl 1277.03011]  \\textit{Stump, Aaron}, Subset types and partial functions., 151-165 [Zbl 1278.03029]  \\textit{Gulwani, Sumit; Necula, George C.}, A randomized satisfiability procedure for arithmetic and uninterpreted function symbols., 167-181 [Zbl 1278.68342]  \\textit{Ganzinger, Harald; Hillenbrand, Thomas; Waldmann, Uwe}, Superposition modulo a Shostak theory., 182-196 [Zbl 1278.68260]  \\textit{Krsti\u0107, Sava; Conchon, Sylvain}, Canonization for disjoint unions of theories., 197-211 [Zbl 1278.68269]  \\textit{Ringeissen, Christophe}, Matching in a class of combined non-disjoint theories., 212-227 [Zbl 1278.68280]  \\textit{Belinfante, Johan Gijsbertus Frederik}, Reasoning about iteration in G\u00f6del's class theory., 228-242 [Zbl 1260.68365]  \\textit{Manolios, Panagiotis; Vroon, Daron}, Algorithms for ordinal arithmetic., 243-257 [Zbl 1278.68272]  \\textit{Cohen, Arjeh; Murray, Scott H.; Pollet, Martin; Sorge, Volker}, Certifying solutions to permutation group problems., 258-273 [Zbl 1278.68254]  \\textit{Colton, Simon; Huczynska, Sophie}, The Homer system., 289-294 [Zbl 1214.68332]  \\textit{Deplagne, Eric; Kirchner, Claude; Kirchner, H\u00e9l\u00e8ne; Nguyen, Quang Huy}, Proof search and proof check for equational and inductive theorems., 297-316 [Zbl 1278.68257]  \\textit{Ganzinger, Harald; Stuber, J\u00fcrgen}, Superposition with equivalence reasoning and delayed clause normal form transformation., 335-349 [Zbl 1278.68261]  \\textit{Baumgartner, Peter; Tinelli, Cesare}, The model evolution calculus., 350-364 [Zbl 1278.68249]  \\textit{de Nivelle, Hans}, Translation of resolution proofs into short first-order proofs without choice axioms., 365-379 [Zbl 1278.03032]  \\textit{Degtyarev, Anatoly; Fisher, Michael; Konev, Boris}, Monodic temporal resolution., 397-411 [Zbl 1272.03090]  \\textit{Schmidt, Renate A.; Hustadt, Ullrich}, A principle for incorporating axioms into the first-order translation of modal formulae., 412-426 [Zbl 1278.03031]  \\textit{Lynch, Christopher}, Schematic saturation for decision and unification problems., 427-441 [Zbl 1278.68271]  \\textit{Anantharaman, Siva; Narendran, Paliath; Rusinowitch, Michael}, Unification modulo ACUI plus homomorphisms/distributivity., 442-457 [Zbl 1278.68246]  \\textit{Choppella, Venkatesh; Haynes, Christopher T.}, Source-tracking unification., 458-472 [Zbl 1278.68252]  \\textit{Pientka, Brigitte; Pfenning, Frank}, Optimizing higher-order pattern unification., 473-487 [Zbl 1278.68278]  \\textit{Schmidt-Schau\u00df, Manfred}, Decidability of arity-bounded higher-order matching., 488-502 [Zbl 1278.68281]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1412856$C8D3CC8E-7652-47D9-9ED8-B24199179D80","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$C2AD60CF-359B-4611-9838-73EC94CD2C1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$C9C633AC-2F84-48FC-812D-72F9321189F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$89542C24-5213-4F8C-93A4-27BDB0D27B19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$713967AD-E5D2-4589-B4F0-38A846211348","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$4CC5210D-DB78-4253-8169-5FAE86E20ED8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"97df35615b375f7498d1bd1e510d12b5917501b9","datavalue":{"value":"2010262","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$A3572BF6-B265-48DD-BE25-74EFC95FECB1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0bf4f74c129274c74f2df90abe98591d25c9e4a0","datavalue":{"value":"Automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1412856$5BB6283E-D6BC-4C62-8E25-EADB7A55D4D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"342d2d38e711d51186d71b367bdd6901f655f6d3","datavalue":{"value":"CADE-19","type":"string"},"datatype":"string"},"type":"statement","id":"Q1412856$AB1E29D8-55D2-4C24-B4CE-3DCCCD349A1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"63c7805d28e68ea1d0da6ab3dbfaa3fd5dd6af07","datavalue":{"value":"Miami Beach, FL (USA)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1412856$CA610622-4EC6-4421-B989-F2F0166988C6","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1412856$DA3A3D2F-817D-40C2-B3D2-4604FE0DA586","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5f2de3997ca74820eaa5379240d8d8210d2079dd","datavalue":{"value":"W2483160171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$8738FC27-A4FC-4737-8445-C45C37CD6138","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"77803cf595c8808153636f8e001b2ddb16a0f0ed","datavalue":{"value":"10.1007/B11829","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1412856$D14E2E9D-BD4A-4F9A-AEAF-71233DFC8C7C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_deduction_--_CADE-19._19th_international_conference_on_automated_deduction,_Miami_Beach,_FL,_USA,_July_28_--_August_2,_2003._Proceedings"}}}}}