{"entities":{"Q1824409":{"pageid":1835151,"ns":120,"title":"Item:Q1824409","lastrevid":73454628,"modified":"2026-04-14T16:03:24Z","type":"item","id":"Q1824409","labels":{"en":{"language":"en","value":"Horn equational theories and paramodulation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4117893"}},"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":"Q1824409$9DA74E45-12FA-484C-82BB-AAAEDFB6C56D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9efe81c78b845fbd83093622332d6fe9ed27ccac","datavalue":{"value":{"text":"Horn equational theories and paramodulation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1824409$F71D5FB3-50A4-4FDF-94D2-DA21D02012D5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"11ea1a457083e43f03af5630fdde222cd15eb7a4","datavalue":{"value":"0682.68091","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1824409$CCAC18A9-4119-4056-8F6B-599FA5DB9F94","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3d552f0d789d7994e4b3d5e7d9013988512a85bb","datavalue":{"value":"10.1007/BF00248322","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1824409$0FB62417-1AD1-4FAC-885F-5CCD9C2D4646","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"41eb43f669c6e9bd047f95552906672fa500745e","datavalue":{"value":{"entity-type":"item","numeric-id":1322771,"id":"Q1322771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$C7D07899-1A21-4BFF-BC38-049BD1F7A335","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d64bfbdd62224172c0dd77b653dc5558f40927f0","datavalue":{"value":{"entity-type":"item","numeric-id":918540,"id":"Q918540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$54394509-350C-49EF-B8D2-524D491046C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a4cb2c91b72706af92b18064760cb26dd7061ab6","datavalue":{"value":{"entity-type":"item","numeric-id":1824408,"id":"Q1824408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$4085C010-63BA-4D7E-82E9-1F73EBBC1645","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$363C3CE4-EE39-4DA2-A596-04086988FB35","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1824409$A3FD55B3-8A76-49E1-8203-4A5AC0156955","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4dc1185f57d65c3df5da67d10a889934ab6cad09","datavalue":{"value":"Robinson's pioneering work on mechanizing mathematical logic quite immediately raised the problem ``How can equality axioms be incorporated into resolution machinery ?'' At the same time much effort has been spent on looking for efficient refutationally complete strategies for decidable subclasses of first-order logic. It was then the Prolog language together with Horn clause logic, input and unit resolution were invented giving rise to Logic programming paradigm. A direct proof for the completeness of paramodulation for Horn equality logic (the language of equational logic programs) is presented. The declarative and fixpoint semantics of this language are then investigated, for the operational semantics the inference rules paramodulation and reflection are proven to be sound and complete w.r.t. the fixpoint semantics. It is well-known that automatic theorem provers based on paramodulation are far from being efficient, since they have to explore a search space containing many irrelevant derivations, since paramodulation can be applied both from left to right and from right to left. The commonly used techniques for Logic programming restricting the search space are discussed and demonstrated. Among them are directed paramodulation, conditional term rewriting systems and narrowing. The paper gives a clear and precise vision of the problems, progress and success achieved in the field of equational Logic programming.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$F6D8571D-E4E5-48B3-9474-C679D430F48E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1824409$C64C4A38-18A6-48A2-9236-A5144FA090C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1824409$06A64362-B84A-4D91-94B4-BBE29881A0D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7fd213a574edd10a6bc470cc2d78cbfa20c5eb59","datavalue":{"value":"03C52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1824409$B8C82ED5-BE37-4B9D-90A4-8A6D7C1A2F75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3dad0277bcd0256d3dcda33e7f0f7f7c58bb6096","datavalue":{"value":"03C65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1824409$30C1A7EF-C725-4A5B-85C5-40E68E56DB83","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2cb83353c02a653b2555f00cda2ff20f8e77e53d","datavalue":{"value":"4117893","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1824409$3A579921-2C29-46E2-BC7D-68E9FD5064DA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$F0537716-B34F-4998-9135-D31D1D712A07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f84bfa4d35417b90f2a3d3973763cb89a42b0a1","datavalue":{"value":"paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$B9548F23-DEFF-4F40-91C8-38B972017636","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff67fedbe8c50d3daca036875aed531217cd953b","datavalue":{"value":"Prolog","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$A0D1EC00-676C-43F1-9084-BFB1AC2A895C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$43A543F9-6856-4D0A-ABEF-D1EC63B7340F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cbd9894bb2ae50bf3e9702ac19cb1c5499b6fe1b","datavalue":{"value":"Logic programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$95BD4CC9-EA96-494A-B61A-8F19F758A953","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"453868b3ecd4cc2ceb48419daecef9c56fc8bd79","datavalue":{"value":"fixpoint semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$353789A6-4C0A-443A-9CAA-3CF1054625D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d4e1e581ddaacb64b25af198d49437baacfeba9a","datavalue":{"value":"conditional term rewriting systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$81E53FA1-CAAB-48B0-AD30-5E749AE10E6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50e20429622ec08ba47dc9e7a4c57de8bf8a42d9","datavalue":{"value":"narrowing","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$E73F0A2F-9C7C-4FEB-9AFA-2826F19CBBC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bd068b4c31803e0d6ae8a49e303f6287677e8693","datavalue":{"value":"equational Logic programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q1824409$22E0CF16-ACB2-4B6B-AE50-C0DC80A4AF4F","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":"Q1824409$CD1F1972-A92F-4083-ACD5-502F71ACE314","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9244cfa0cc83c54f6dddc3fcd9671a0260655de","datavalue":{"value":{"entity-type":"item","numeric-id":3942361,"id":"Q3942361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$ADE1A0EA-DFC8-4AF4-BE2B-52A39298511D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4fb53dc30cdc46111c93a6e7de143f2e9b39160","datavalue":{"value":{"entity-type":"item","numeric-id":4099229,"id":"Q4099229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$64D13E8D-5F37-4702-8E8B-83186D9C6F56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$1FD33EAE-C56D-4F0C-AB49-5B8F1A0DA03F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61ba87c987c84ca4579443b762c28d920c8ce683","datavalue":{"value":{"entity-type":"item","numeric-id":1087023,"id":"Q1087023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$5E91E692-353B-4874-BFA1-C63AF3722357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5f91daa2195cbe510cefc59ffaafa18b1c28390","datavalue":{"value":{"entity-type":"item","numeric-id":4107888,"id":"Q4107888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$9982380C-7E19-4EF5-9992-541E778D3ABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c1b55d8f43ca125643590f04b775951f5864389","datavalue":{"value":{"entity-type":"item","numeric-id":3692850,"id":"Q3692850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$CF63E811-9FEC-47A4-93DC-94053C819CC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c7c626276619186e4feb1c0613ffe3d9280b757","datavalue":{"value":{"entity-type":"item","numeric-id":3765264,"id":"Q3765264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$189AF8C1-0F3E-43D1-AFB1-3AD5D36B78CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bd833b39da4bbfb545ee75e04b0eab6b1bce596","datavalue":{"value":{"entity-type":"item","numeric-id":3821637,"id":"Q3821637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$F1D2E3F5-960A-4F51-9271-5FDF387EADE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa80180d2b637ed45ce99d0a3160b0b2727285e","datavalue":{"value":{"entity-type":"item","numeric-id":3782762,"id":"Q3782762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$3C0F7838-F3EB-4370-84E5-98FA3EFE5F26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"604fc502056f8cc2ccfd9332e67d94de225503f6","datavalue":{"value":{"entity-type":"item","numeric-id":3789061,"id":"Q3789061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$098DE58A-0669-4F82-941D-6C31E3A7AD2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6249290c793fa3d4c305541f1a11cd397a401609","datavalue":{"value":{"entity-type":"item","numeric-id":5902880,"id":"Q5902880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$57464A0C-F9AE-4988-AB38-52BA7DB0B6E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"041184ced68ec1bcfc7e3558db4714d4dc908858","datavalue":{"value":{"entity-type":"item","numeric-id":4050192,"id":"Q4050192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$3404634C-620C-478F-B5AB-87BC49F3F7EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e9acb750b5a1fcf5fe08b591fc6df182dd9e5e0","datavalue":{"value":{"entity-type":"item","numeric-id":3883561,"id":"Q3883561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$85E9212D-7547-49BA-BDA5-00222FC9FC11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de57064dff6d8c801eaa4cbe8a91d55ce2cc76c5","datavalue":{"value":{"entity-type":"item","numeric-id":3703312,"id":"Q3703312"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$1B719C08-0C43-45F0-B60E-DF51C38819DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08494127cebe2a7e5cd00bb77f9a92192bb264cc","datavalue":{"value":{"entity-type":"item","numeric-id":3707362,"id":"Q3707362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$BBE14976-9065-40D8-84E3-5693E9C3AC8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c9465d6417bb77bd19e652eaf6c381784d12e8b","datavalue":{"value":{"entity-type":"item","numeric-id":3936229,"id":"Q3936229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$BD46B9A0-BD61-4205-8ACD-CF0A13648E9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03dcc815537b517cc71ed958068897d2b199f6d8","datavalue":{"value":{"entity-type":"item","numeric-id":3339245,"id":"Q3339245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$E45F974B-A750-46D2-BCC6-70C344490E04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5939193d2c734f0c40871d2dae732bc5d8448c2d","datavalue":{"value":{"entity-type":"item","numeric-id":3673152,"id":"Q3673152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$6D5235B4-D14C-47E9-9BAE-9B7140B2B9BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10514d04294539f6b18e653ffed15729ce3e519b","datavalue":{"value":{"entity-type":"item","numeric-id":5678447,"id":"Q5678447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$C99A7AEA-616C-42C1-9CAD-FDEE0D68ABBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febe5bf101c3b7d6dce19439eb466caa5715de79","datavalue":{"value":{"entity-type":"item","numeric-id":5624683,"id":"Q5624683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$99361C41-8131-41B0-A896-4FC7F12D463B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$FCBC62C5-BEF8-460B-9A66-E9CAA4CBBB08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db57d83c4539b5e1e312a9885e87a573f21cf309","datavalue":{"value":{"entity-type":"item","numeric-id":5562604,"id":"Q5562604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$597EB97D-D087-4CF7-8766-7D986863FF06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40b422d2d294023b23695a8b39e822af284cc280","datavalue":{"value":{"entity-type":"item","numeric-id":5639371,"id":"Q5639371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$C9F62A5E-5944-43AB-83E5-759A40833A02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3dac14c70bb691f81b7dbe3b97332456bc88540b","datavalue":{"value":{"entity-type":"item","numeric-id":4770009,"id":"Q4770009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$104E0F77-60F9-4CDD-8683-C26BE3F7692A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7053c119e620b9c3b3c8c19da3a6a2d1be1e3c68","datavalue":{"value":{"entity-type":"item","numeric-id":5538934,"id":"Q5538934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1824409$DDEA4238-4A5C-418E-A5D1-8DFCC62853B1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b81381978311278b966f7bc36f3c036bb7c499c7","datavalue":{"value":"https://doi.org/10.1007/bf00248322","type":"string"},"datatype":"url"},"type":"statement","id":"Q1824409$8B3BBEC8-3B81-451C-AD7F-9458CE8E749E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"58beb3b12d69c9643684435b53221474c154434f","datavalue":{"value":"W1967047591","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1824409$42CC94F1-BA0B-4E5D-8154-0AE32AAAAFA2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6e120e715734180afc3ab140168d58ad33395fb","datavalue":{"value":{"entity-type":"item","numeric-id":1801319,"id":"Q1801319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5da3fd5385fba0f5da220fc1297c85866e9c8784","datavalue":{"value":{"amount":"+0.846846342086792","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":"Q1824409$A7B1E886-D6AB-434D-ABC2-DCAAAB15A37D","rank":"normal"},{"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":"a0de1e411b685da6922246c58bfa871b1067e74e","datavalue":{"value":{"amount":"+0.8158401250839233","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":"Q1824409$8A12D9CC-BADA-4A58-818F-2181E35A216D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4564dcbe209d24a2f509e63518773f769d6b6c9e","datavalue":{"value":{"entity-type":"item","numeric-id":4524792,"id":"Q4524792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92e857e66899033dc532cb7d29c91dedf6689b24","datavalue":{"value":{"amount":"+0.8154347538948059","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":"Q1824409$0DDBA47B-4283-4764-BC84-1CED9734E797","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":"7e2d9cde3b5f0f16e1f5bfda9ee0d637c22dcf6e","datavalue":{"value":{"amount":"+0.8146581053733826","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":"Q1824409$020E4F4E-2172-490C-9E83-767EBF33D798","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d37075a1917e2553c5f07df3e33a3ba49fe52029","datavalue":{"value":{"entity-type":"item","numeric-id":3707362,"id":"Q3707362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e9cc276b03c4bed8b4a56fd95ea571b450b149a","datavalue":{"value":{"amount":"+0.8129506707191467","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":"Q1824409$52E16EEC-2F56-41B9-8D80-CE92834167BB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Horn equational theories and paramodulation","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Horn_equational_theories_and_paramodulation"}}}}}