{"entities":{"Q2486578":{"pageid":2497321,"ns":120,"title":"Item:Q2486578","lastrevid":48525031,"modified":"2026-01-05T02:52:01Z","type":"item","id":"Q2486578","labels":{"en":{"language":"en","value":"Translation of resolution proofs into short first-order proofs without choice axioms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2193209"}},"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":"Q2486578$01115563-3988-4EFC-BF33-5D26CFFCF2C7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fa9fa33444e05c0506434a7e379650d1b00a6d2d","datavalue":{"value":{"text":"Translation of resolution proofs into short first-order proofs without choice axioms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2486578$F80CFEAD-B062-4F53-A4AB-9614B6C0D427","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9509b3b59a511c54717869dc4f9887300998aeeb","datavalue":{"value":"1081.03014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2486578$BF094447-49C8-49AD-8B37-C9ACD35FC756","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0af7e025189305bad11f686c710fe3b187470eaf","datavalue":{"value":{"entity-type":"item","numeric-id":438567,"id":"Q438567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$C36DE467-54EE-458F-9D22-B9959CCBBE0E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$BE37641D-38F3-4A92-A879-730D8B71B337","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"90b8e08a65c3f6b60302137bec886dcfcd8ff418","datavalue":{"value":{"time":"+2005-08-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2486578$CA240A4C-B964-4F6C-93C6-C4B9B8C1E9E4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2486578$BA0C8612-5FED-467C-88C4-4AE4040AF836","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2486578$F4DABD15-CBB2-46B5-97E7-BD34800D592A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2486578$010CDBC8-C450-446F-AE6C-FE5F1AC48275","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0401382c22a8a7ef4304d5368c48dc351c801513","datavalue":{"value":"2193209","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2486578$390AF8A5-54A1-41DE-B0D3-9D31CE4E2FB0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"742acadec2058a1daf33969cf122f1e00d23a668","datavalue":{"value":"Theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2486578$8A56A7C6-7E1D-488B-AB82-938FBD1FC094","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2a0cbbc442fcc127d9fa405ab5ed2ad80336e2fc","datavalue":{"value":"Proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2486578$242BDDA8-D470-45A2-8271-96DC44BEB396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b34e81c9be74c25aae2603a8dfa343c349c2721","datavalue":{"value":"Skolemization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2486578$6F9A8D47-AC96-4B42-9EBD-78A7EFAAAB6C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$1055CC76-D62A-4F7E-BFE4-99002381DC5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"233bd03fc74bc4c01e6f828569e5eb13f94bb747","datavalue":{"value":{"entity-type":"item","numeric-id":22242,"id":"Q22242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$8506A637-6D5D-4B7B-A342-E1046A4EFFD0","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":"Q2486578$CFBD317F-E483-41E0-A296-6BCB00DC8D05","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0db0155ee39ac87d5c13edc088e76a672ff55b68","datavalue":{"value":"https://doi.org/10.1016/j.ic.2004.10.011","type":"string"},"datatype":"url"},"type":"statement","id":"Q2486578$EEF5F620-CB10-449C-9043-E4E9295AADA7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aee6ddc356eecbb706c8734ea4bb4592edec1d9c","datavalue":{"value":"W2093910552","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2486578$3BD5BBFD-23D6-4F5C-81E0-4887C0D3BA82","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9d43b2a1f5b23f5e07e09c2947ef1c6f323b764","datavalue":{"value":{"entity-type":"item","numeric-id":2751356,"id":"Q2751356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$C72ABA8B-3D24-4E21-ADEA-3761630FD55F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b559e594edc07777117cb084e905ea94187a1df3","datavalue":{"value":{"entity-type":"item","numeric-id":4304753,"id":"Q4304753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$A7580C47-279D-46AB-9CAE-334A383EBC9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ad7c23e8d7895495a33ef0a244c1d5f7a7d7e16","datavalue":{"value":{"entity-type":"item","numeric-id":1899908,"id":"Q1899908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$7309FE04-E11B-41A8-8499-335BFC93154D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be126e0eb8d13204e0b0a96acc72543ab758d244","datavalue":{"value":{"entity-type":"item","numeric-id":2723415,"id":"Q2723415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$1C20E20E-C779-449D-9A40-CF0D9B401E54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4678e4c2f003554895218494da0c1f6e87bb3ea","datavalue":{"value":{"entity-type":"item","numeric-id":1868508,"id":"Q1868508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$FFEF73C5-02E2-483F-9BEF-165D7348BF8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"90bc06dbf3731697a67c4cf4f2c88c3e70cd5b2d","datavalue":{"value":{"entity-type":"item","numeric-id":3136460,"id":"Q3136460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$D9E70E90-7904-47E0-9D8D-EFB705CFF93E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18cdec34fa64c4fe94079af9a70deb0327c75541","datavalue":{"value":{"entity-type":"item","numeric-id":1201346,"id":"Q1201346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$1B0A98F6-5540-4CEB-A963-1C6B4277238E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"94812d36ec09ea0d0621647bede0c34a09d4d46f","datavalue":{"value":{"entity-type":"item","numeric-id":4411849,"id":"Q4411849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$22597555-DC3E-4FAF-8DAE-6834A16AA125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c821e2f215bc80251a106b233aa765932eff23","datavalue":{"value":{"entity-type":"item","numeric-id":5900728,"id":"Q5900728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$B77E9B5A-1974-4F53-BD67-12CD8654CE89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f14878b4342799995051ac9bc54cd21c98efc98","datavalue":{"value":{"entity-type":"item","numeric-id":2751359,"id":"Q2751359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$6CFCF42C-2A2A-4754-BCAF-6622829C187A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28deebb9f03725888e2cb415bbaa29688963935e","datavalue":{"value":{"entity-type":"item","numeric-id":2751358,"id":"Q2751358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$E8825FA2-9093-4880-88F2-69DB377D0217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86e2b29d9b4dadfb2f5b72715f7422f8e108a4ff","datavalue":{"value":{"entity-type":"item","numeric-id":1167721,"id":"Q1167721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$B7D19AF4-93FC-4756-9F2E-7CE48BC28A4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58cb14dabb49ce81b914063d4d765de30bcb45f7","datavalue":{"value":{"entity-type":"item","numeric-id":3338233,"id":"Q3338233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$95019FF4-4240-455C-B645-448126082E52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54610551b079750a1912b04c566b7c8cb84a1b21","datavalue":{"value":{"entity-type":"item","numeric-id":4809051,"id":"Q4809051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$0183BA88-293E-4398-8CE0-A4BD3C8B611A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1813c495b4019dbc5a0338bf865711982b775489","datavalue":{"value":{"entity-type":"item","numeric-id":4198750,"id":"Q4198750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2486578$51333E0D-3871-45D2-881A-1B75166B995D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e971a32155f46bc80290fb303f45a1244f9e0506","datavalue":{"value":"10.1016/J.IC.2004.10.011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2486578$04882561-3B7C-4FE8-A745-8F4F2BBBB037","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"990e4835b2ff0f74d6d2c7fd14a4cd2b0a6f0f4e","datavalue":{"value":{"entity-type":"item","numeric-id":5900728,"id":"Q5900728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3e8500834f1a54becba8bb462fcce08b8b81f38","datavalue":{"value":{"amount":"+0.9943276047706604","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2486578$088DBD0B-719A-4CC5-8695-3CA2ECB3102B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0f90d678a6e317f374f8cce2229fe81591e5210","datavalue":{"value":{"entity-type":"item","numeric-id":3525003,"id":"Q3525003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"433216d4d616cff6b5515933847a5164488cd6a5","datavalue":{"value":{"amount":"+0.7929999828338623","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2486578$9659B678-E036-4869-8896-0D4EA1171571","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8fad119391ac0650fa8016c1ceba6481f2374b2","datavalue":{"value":{"entity-type":"item","numeric-id":3777987,"id":"Q3777987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2363773476374e647f38db9dd44b970c81a43de8","datavalue":{"value":{"amount":"+0.7848829627037048","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2486578$22F1DB26-C1CE-4E6A-B0CE-2975DEE1B725","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b6b6f5f0ca85edeee446ec0c09180658cfcac311","datavalue":{"value":{"entity-type":"item","numeric-id":1098330,"id":"Q1098330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ada904c750b407ea9b4ad64143829ff12febc961","datavalue":{"value":{"amount":"+0.7582058906555176","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2486578$B9743A98-77DF-4BA0-AC0F-3D8A8711FFDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad1fb78904ad2e2d3511117dee4a1123476c2652","datavalue":{"value":{"entity-type":"item","numeric-id":972424,"id":"Q972424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"419433da46383445a86e49287f0483b185f218a8","datavalue":{"value":{"amount":"+0.7542627453804016","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2486578$27DAD932-6022-4974-9DB3-97A21343C9EA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2486578","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2486578"}}}}}