{"entities":{"Q1328182":{"pageid":1338932,"ns":120,"title":"Item:Q1328182","lastrevid":43032471,"modified":"2025-07-17T01:59:09Z","type":"item","id":"Q1328182","labels":{"en":{"language":"en","value":"Refutational theorem proving for hierarchic first-order theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 599669"}},"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":"Q1328182$EEA09FD9-9FED-49F9-A9C3-63042197FD87","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9b5b52b3725dd24621d8342a7f60d2861e6a0a76","datavalue":{"value":{"text":"Refutational theorem proving for hierarchic first-order theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1328182$6129D8E3-C5D2-4A6C-AA0A-48E08A12FC53","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8b21b115bfe2a226ad8b6eb78225029fc6f5b48c","datavalue":{"value":"0797.03008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1328182$05A4449D-BB82-4553-AEF1-4225C366A9E3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f1aa88660c4181fb73b1ebb8de6daef0cdd79de4","datavalue":{"value":"10.1007/BF01190829","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1328182$E7BA51D4-6853-42DF-8F6C-4D644D16099A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0cf815526c4f2604ee47e98322610a52470dc8b3","datavalue":{"value":{"entity-type":"item","numeric-id":1072370,"id":"Q1072370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$2010E0A1-3580-4A80-9B26-000E95EDE617","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b043e7c633006f3fac5c3bfd0395a92f663b5539","datavalue":{"value":{"entity-type":"item","numeric-id":758210,"id":"Q758210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$3A08912F-25EC-4268-8066-CCF953CC5EAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ecde3ddf4f96a8da457aeb906b2979614b354694","datavalue":{"value":{"entity-type":"item","numeric-id":293310,"id":"Q293310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$C87AAF1C-DDDC-47CC-8C9C-FE21A89D7237","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e71b1a810c94176f33b214acd409208085d409e4","datavalue":{"value":{"entity-type":"item","numeric-id":162945,"id":"Q162945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$5C1FEAA5-4678-4E7D-9B25-7DD3603D832F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8b439a09488bc2e6cdbf4d00c3a7f90f1bcfc4c1","datavalue":{"value":{"time":"+1994-07-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1328182$5BB3CDC4-576C-48C9-82E1-ACD25B01A5BF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1328182$AF1BD1A3-27E2-42EB-B7E1-3B5032B58DB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1328182$219B3E25-651A-453A-B07C-48B93B726785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1328182$BFC3180D-0373-49B5-ADB7-092C3AFDFFF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1328182$B394EE48-1131-4A18-8A27-33CF8ABF45F2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6a28f4aaabf783a408c2f163b511a54b25459117","datavalue":{"value":"599669","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1328182$984A60C6-32D1-4880-B65F-407DF3F34F3A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$57BD2B11-0C28-4CD1-91D5-28F820EB3C9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc84523e41a1c93f98d4ea541c8bba23fa54716d","datavalue":{"value":"constraints","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$F9DB8C2E-0278-45E5-AE0E-E5C292ECB2F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ce94254d44045733e962d2861c33d94e3725cca","datavalue":{"value":"quantifier elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$67A46E6D-C0ED-4ABF-95BF-B578DF6D533C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$D76E38E1-3E40-423F-B953-4DD81C71396D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47aefda07ac5d6e74103bdf2455b1df41b0e324b","datavalue":{"value":"algebraic specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$B6551FAC-3AC6-4ECE-B8A7-04E660149F0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51a5b03158a89e6bca8e0c5282a45005ad999917","datavalue":{"value":"hierarchic first-order theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$ED0199B8-6551-4DEB-B0F2-0A18A55F9C98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d86a171fa82c1ea15db4e7a7c23402cbb117f3b1","datavalue":{"value":"superposition","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$DB742E9D-D46A-4F45-9E7D-A200E1CDED72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9a2e0a24d33cc55a1243bda19886e6ac508bc07e","datavalue":{"value":"variable abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$E7C8D316-825D-4861-A8F2-70F107574F6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd0c8a1dd727b7d5afda034e63236a665c03b913","datavalue":{"value":"constraint refutation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1328182$804A651E-D3F5-49E1-BB33-69ED5D3E03C7","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":"Q1328182$2D793414-CB61-4729-92D9-C32CE4895C27","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcee6c84e9331eb414de7a5dee6a2dd582369033","datavalue":{"value":{"entity-type":"item","numeric-id":3912001,"id":"Q3912001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$7407F36A-06E2-4324-B17B-16AAA34842BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f4eb651c8363807599380b2222eea5dd308b21b","datavalue":{"value":{"entity-type":"item","numeric-id":1596540,"id":"Q1596540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$116A12CB-6FD8-404B-9793-44F4A04F0724","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af2858b2caeba0cb898fe2f4f9cbcd3fd3b0230e","datavalue":{"value":{"entity-type":"item","numeric-id":5536619,"id":"Q5536619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$E6ADC689-88B5-47BC-A9D3-3D73C6FF8029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3980c1d1000e274389019d30f2493938b8c9d56","datavalue":{"value":{"entity-type":"item","numeric-id":1182107,"id":"Q1182107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$D3604B6E-9C32-48FD-9273-7335370F2B94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27ee3b057142576093bd9e66364057980fafc0e4","datavalue":{"value":{"entity-type":"item","numeric-id":1821564,"id":"Q1821564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$78EE0F55-D1A2-48EE-B745-D6B424FB1283","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8510bf8d385867652fe1ff910f60e49509ddb12","datavalue":{"value":{"entity-type":"item","numeric-id":4342096,"id":"Q4342096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$9DA3238C-15A8-472E-930E-4538700689EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c1c64aa77167c6580cd7c8c676f0c865faa32857","datavalue":{"value":{"entity-type":"item","numeric-id":4385539,"id":"Q4385539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1328182$E65470B8-CEDE-464F-A839-8F53CA5AA283","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1f91f2a04af7ed716280a69b31bd5722b64e604","datavalue":{"value":{"entity-type":"item","numeric-id":4246725,"id":"Q4246725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a7c6a1d31eaf092bb3748c2373ccd1bbec11e3a8","datavalue":{"value":{"amount":"+0.9494283","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$DD23093D-69AC-409F-BA10-4F1E326B701E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9e040b69366aa385ecb7819d5a979d92c0954fb","datavalue":{"value":{"entity-type":"item","numeric-id":3805955,"id":"Q3805955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97dcb19170dda57bde22d95660b9e7f09a71af16","datavalue":{"value":{"amount":"+0.9123488","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$908A4E6C-08D9-404A-9CE9-0B9EFE600350","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ecbedcfe3626185d0bb331b094353198a89395","datavalue":{"value":{"entity-type":"item","numeric-id":802317,"id":"Q802317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97dcb19170dda57bde22d95660b9e7f09a71af16","datavalue":{"value":{"amount":"+0.9123488","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$4702B114-C18B-46FF-A2B0-455EFC7FB1E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d6d293412ec27137e9c499546b1328aad012c7d","datavalue":{"value":{"entity-type":"item","numeric-id":3133155,"id":"Q3133155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88e753adf641b4482fbd7daf3c67b2a55b323402","datavalue":{"value":{"amount":"+0.8938523","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$D6D0E022-DEA7-470F-87A2-F6628E2A9AEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ecae2da48cc5077a2cb61d68469a5ebeeb0ead5","datavalue":{"value":{"entity-type":"item","numeric-id":4336265,"id":"Q4336265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"564c509599720cae430807659e91bdc508c01363","datavalue":{"value":{"amount":"+0.8872088","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$5F484B84-9C3D-4A90-8F23-2C5463305995","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3858e1634101a8fbbcdac056ef503d49e96eb9b","datavalue":{"value":{"entity-type":"item","numeric-id":5884936,"id":"Q5884936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aca201e2e76ef1b0dc364560da3d4f1fc78ee41c","datavalue":{"value":{"amount":"+0.8846889","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$0FB7E804-6C0E-47A4-B480-9841F42038AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab683a7b1f35576127c529e6651dcc1403e6eaef","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87b6b7237796c48f66d24051b865cd0cd1bc3384","datavalue":{"value":{"amount":"+0.8824055","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$473A17E6-E5B4-4025-B07B-CAB527FEB6E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d99375d9af310691fe93cef97a2d130b782c085","datavalue":{"value":{"entity-type":"item","numeric-id":3472096,"id":"Q3472096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b863a5a478f0e1117a51da6f31264b46fec70fe","datavalue":{"value":{"amount":"+0.87989384","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$1C4863E7-992C-4AE4-811B-54F7BA23B59E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"93d096a65db3336b7d8e636037731ead644dad76","datavalue":{"value":{"entity-type":"item","numeric-id":1272612,"id":"Q1272612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea41a3d4bb7a87928a120d018c678b97c0b0806b","datavalue":{"value":{"amount":"+0.8794837","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$F489BEB0-FE12-4D73-895C-569BA74EBD63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ddcd94f921aa20f6b9b45b22d22d4796be094a6d","datavalue":{"value":{"entity-type":"item","numeric-id":429582,"id":"Q429582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a7f042a3ee5fa2985ca1d08ec857fb56546d7e74","datavalue":{"value":{"amount":"+0.8794776","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1328182$D555A886-C37A-42BD-A427-5148C10737B2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1328182","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1328182"}}}}}