{"entities":{"Q1897557":{"pageid":1908299,"ns":120,"title":"Item:Q1897557","lastrevid":69073920,"modified":"2026-04-13T04:28:09Z","type":"item","id":"Q1897557","labels":{"en":{"language":"en","value":"Theorem proving with ordering and equality constrained clauses"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 792836"}},"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":"Q1897557$567B6808-12BD-4E40-8889-5188326C31E7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"67b2fa80d182c951e0b4a1cf6fdad7fba49c9943","datavalue":{"value":{"text":"Theorem proving with ordering and equality constrained clauses","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1897557$AACBCF60-A06F-4A05-A424-957B8696A06F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f10cfba1a13e700a6db5f4b659f003427a6fe66c","datavalue":{"value":"0844.68107","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1897557$218C9EDF-0AEA-4EEA-B9C8-876D5DD65210","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1e6a58ff964b9ca97414f0c42659717fa8e6fc43","datavalue":{"value":{"entity-type":"item","numeric-id":475169,"id":"Q475169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1897557$0AD4C81F-B0A6-438A-8BFF-391397742C1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"076f42ceb107ac95ece0987fd254ab37feda8487","datavalue":{"value":{"entity-type":"item","numeric-id":352976,"id":"Q352976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1897557$3A1B4D4C-055A-4239-8249-8DE1C626452D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1897557$5A921733-1A1E-4AA9-A66D-CD9316933B3B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"898ac30877e36053f36ef2832809d3bd0f936548","datavalue":{"value":{"time":"+1995-09-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":"Q1897557$9E1DE1B2-AADE-458C-87BF-87F4872F4BDD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"37272b17d7ea854fa165b8f30cdcbb52cbcc66a3","datavalue":{"value":"https://semanticscholar.org/paper/06e483d04ec418ded7719bd9af4e42e07c325b53","type":"string"},"datatype":"url"},"type":"statement","id":"Q1897557$FAD73AD3-1130-4933-B91B-1F3759CD1382","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1897557$D9D3B421-F993-44FC-A31D-E31656442003","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e0cdecac5e3c7018c283e3e655394d67a09cc6ac","datavalue":{"value":"792836","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1897557$C0CF80D2-8E3B-47E0-8FC4-40284EF1ED6B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f618c1719dd6f7717b9ba9ef55900319e2884d92","datavalue":{"value":"constraint strategies","type":"string"},"datatype":"string"},"type":"statement","id":"Q1897557$1F1B934F-3784-4640-94D3-8D6268DC54ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e09b5347b1310da0b709d67c68bb0f5d7fea817","datavalue":{"value":"constraint inheritance strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q1897557$1DA4E91C-ADD4-4ED6-A4BE-3D7BA383E09A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"053337c195ecace05843fce07fe604559482dd00","datavalue":{"value":"redundancy criteria","type":"string"},"datatype":"string"},"type":"statement","id":"Q1897557$C87EBFDA-B768-4EBF-9994-BD9805CB2063","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":"Q1897557$F117EA65-0D45-40AF-9AAE-0811D1D1417B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cbe1fec601dc1452db345a12111417bd77ada685","datavalue":{"value":"W2082976889","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1897557$C3E1E28B-C02E-427C-923E-08BCA56C912D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b53078a5c3557abd030277ab439ae6a68fd30485","datavalue":{"value":"10.1006/JSCO.1995.1020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1897557$45EBB114-6B66-4ED4-A7C5-0FA46032E40E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6bf56b202a92a35163646cc31fe57791a6a63a51","datavalue":{"value":{"entity-type":"item","numeric-id":4012174,"id":"Q4012174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4662991b3432881c9e40906f198fd2f549c49ff5","datavalue":{"value":{"amount":"+0.8062887191772461","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":"Q1897557$A77C9C4C-5D75-470B-937A-9076D0EEDA2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"319e919e54ae19af5725b0d7ca2380a762f4acbd","datavalue":{"value":{"entity-type":"item","numeric-id":1182107,"id":"Q1182107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fd8e36e102f6b33c0ddf10d06c1f38068e749953","datavalue":{"value":{"amount":"+0.8013521432876587","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":"Q1897557$2BF06F09-0311-4BC5-967C-0CFB3B6A392B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"663b4e5a63cb4379d9ebb8567a8fb5f4ba79e6ca","datavalue":{"value":{"entity-type":"item","numeric-id":757094,"id":"Q757094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b081288a9671a263b6a9188bf144b9efa2fc115","datavalue":{"value":{"amount":"+0.7981247901916504","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":"Q1897557$20EB8D09-98D4-4B85-988C-871BC9808B9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d8cdcc0bc38cde26587a3338b1faf976e3f210f","datavalue":{"value":{"entity-type":"item","numeric-id":5881276,"id":"Q5881276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"851e671e21894e1737ae161312b951b207cb5659","datavalue":{"value":{"amount":"+0.7928756475448608","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":"Q1897557$92E17D7A-007F-4FEC-9333-C246AD84BCA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"126f7aadcf86a4abb574c1835ceb3af729a14aa9","datavalue":{"value":{"entity-type":"item","numeric-id":4255513,"id":"Q4255513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25d8e437adaa6c9673cc57082d99bfe84db268ee","datavalue":{"value":{"amount":"+0.7757176160812378","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":"Q1897557$CC3FFD97-44FE-4E41-A0F7-29169202ABF7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theorem proving with ordering and equality constrained clauses","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theorem_proving_with_ordering_and_equality_constrained_clauses"}}}}}