{"entities":{"Q1960430":{"pageid":1971172,"ns":120,"title":"Item:Q1960430","lastrevid":47430136,"modified":"2026-01-01T17:52:08Z","type":"item","id":"Q1960430","labels":{"en":{"language":"en","value":"Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1387355"}},"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":"Q1960430$512FDC9C-2C5F-432C-80CA-365254B34D51","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"72268650d53df8491359796de9ed83cb75b78c07","datavalue":{"value":{"text":"Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1960430$AE880034-0759-44ED-A830-D77CE2546A31","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c5b3329f9f5c18f5522830e849aad4e4db2059fb","datavalue":{"value":"0937.03020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1960430$98C77DC0-2996-412F-AF71-44482436CB27","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4892d6ca4dac6158085a821963cac8899b25201c","datavalue":{"value":"10.1016/S0304-3975(98)00317-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1960430$DB5D7B93-589B-45C2-8037-91BF0DC650DE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bab2dfee53655d9cc8087a652185465cb178825e","datavalue":{"value":{"entity-type":"item","numeric-id":229754,"id":"Q229754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$E70592D6-18BF-4B67-9FC4-6787DD5B58DF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$0DB34BA6-82AF-4FF1-8B4F-9B885EA7ABAB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"195732dcabfbab6a027b397db48d9b246fab9fe7","datavalue":{"value":{"time":"+2000-01-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1960430$2ECA940E-9B64-4333-A81C-4598B8C47456","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"586227a80c130eae53468d6b914385ef784d2656","datavalue":{"value":"Herbrand's theorem is one of the major tools in automated deduction in classical logic. The tableau method, the connection method and model elimination are based on a direct use of this theorem. Variants of Herbrand's theorem are used in completeness proofs for nearly all methods of automated deduction, including variants of resolution.    Recently, a number of results about Herbrand's theorem and proof search for logic with equality have been published. This article aims at presenting results in this area and filling in proofs of some results that have been announced but not formally justified.    We also give more precise formulations of results with respect to the signatures in which problems are formulated and provide a table of known results.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1960430$22BEFDB0-654B-4F48-8FFB-0934260C1E04","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1960430$DC33B805-3F38-489E-8327-AD1B1762910F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1960430$BF1B22C8-8AF5-4E89-9E91-8C8D3D180F0F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ff6b90cd0afd21d9e2aae7a404b1994ff13fa25d","datavalue":{"value":"1387355","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1960430$63214577-A57F-4283-ACBF-72E964D4908F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9503c637b69eeb659e8970d203497332fa5acaac","datavalue":{"value":"rigid \\(E\\)-unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1960430$AEEFAD1E-26AA-4E7E-A60B-330A8C292983","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a09c1984b41935c0a923dca51c0af0797d5eb50a","datavalue":{"value":"Herbrand's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1960430$C057856A-5F84-43E4-9429-27305C2C9BDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1960430$BB464969-916D-4AE5-834D-1D1A5C2B695B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4879e8c35d56fd297a402f7c1eba53238e04d57b","datavalue":{"value":"proof search","type":"string"},"datatype":"string"},"type":"statement","id":"Q1960430$76A114EE-D8AF-4AD2-B4DF-A41EAF7FDB6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7893e357e06406a1ab747918b4281635a4030099","datavalue":{"value":"logic with equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q1960430$B61052A0-D756-4662-9A14-846F79E255C6","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":"Q1960430$E3E2CF4F-C6A2-469F-AF4A-4E3C1D41FEBD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"818f2044ada61f8186028673bf007a526a9aea73","datavalue":{"value":{"entity-type":"item","numeric-id":4096457,"id":"Q4096457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$8D61B1D4-810B-4A31-A28C-440B3311B8C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea89222d9022292d1ae628b55b56ffd59e9f0028","datavalue":{"value":{"entity-type":"item","numeric-id":3140630,"id":"Q3140630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$F02310EC-5572-425F-B5C6-A69B4CE4C677","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bb24ef7f10a33dfe95076d3ff93619b47a1648b","datavalue":{"value":{"entity-type":"item","numeric-id":4113824,"id":"Q4113824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$84A86A56-0B76-4941-9F3D-1055F8EAEC83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82285947ecd1d65d80e17696025cdf5ddb799be6","datavalue":{"value":{"entity-type":"item","numeric-id":3922205,"id":"Q3922205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$271161E8-424A-4054-9BF5-F4C89F831886","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af4555c0d89e243a8a9351cedc1b4ffbfceace09","datavalue":{"value":{"entity-type":"item","numeric-id":5691140,"id":"Q5691140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$2C2415E9-F13F-4404-9E15-239870200B95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"508ce1a717805f25357aee0cc5c80d75f0475557","datavalue":{"value":{"entity-type":"item","numeric-id":1575636,"id":"Q1575636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$92BBEFAF-5BEA-424D-9419-5F2AFDA29AB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d06d5d70e468a6e54f842447d789e389fefee5d8","datavalue":{"value":{"entity-type":"item","numeric-id":3838767,"id":"Q3838767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$29E139FD-6267-48E1-8983-D12F771C33C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4883090fee4a18fce37441e60e7576f14bdf3e01","datavalue":{"value":{"entity-type":"item","numeric-id":671659,"id":"Q671659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$3E400CEA-7877-4A24-B8E8-2D90CFE47AF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e81d57b58abc3a82b100d072439fecb147f7ea86","datavalue":{"value":{"entity-type":"item","numeric-id":3716320,"id":"Q3716320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$ADED81AA-1173-4F0E-A118-4D503F2E5CD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"156b827ac08590a45280d67b6908c8fca5d0899c","datavalue":{"value":{"entity-type":"item","numeric-id":3796803,"id":"Q3796803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$C6DE90C3-4C38-476D-977F-38B3024A1C4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe4c1ea89bc5854f421d3a6b161146d5aecefa12","datavalue":{"value":{"entity-type":"item","numeric-id":4032862,"id":"Q4032862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$8F678083-83D2-482F-B066-BCFA68B249E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a37da6481d3393a5a430cfe31bbfd3e1bb865a00","datavalue":{"value":{"entity-type":"item","numeric-id":4380444,"id":"Q4380444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$66619C82-27D0-4E9E-B0D8-9A8B16C9BA8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7021c91f6a866e16b579f74b23aa54446a0c8938","datavalue":{"value":{"entity-type":"item","numeric-id":1150586,"id":"Q1150586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$8911B5AB-3802-42FC-A051-C3ACB2BB3C5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ed8c187a7ee81de4810767d03dfff5dfedef859","datavalue":{"value":{"entity-type":"item","numeric-id":4571948,"id":"Q4571948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$5B7C4DF2-63EE-4456-86AA-989A7076AAED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b83592ffe861aca3198948b3c2b96ca5082aefc","datavalue":{"value":{"entity-type":"item","numeric-id":4272505,"id":"Q4272505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$7533E694-72D7-4964-86D0-30EA690626CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2edfe8015b58c579c54c78cbe4fe122a242df00f","datavalue":{"value":{"entity-type":"item","numeric-id":4152529,"id":"Q4152529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$0EFAADFF-2CFB-4B55-A6B7-9386BF695081","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86593a96a302fb40be911c0dc2f6191d2a756593","datavalue":{"value":{"entity-type":"item","numeric-id":3960661,"id":"Q3960661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$C76FA4EE-A70E-4A21-8BFA-87D5581EDA56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a40f91ca37c12613fcd635dd4df7df40dd8c7eef","datavalue":{"value":{"entity-type":"item","numeric-id":1252236,"id":"Q1252236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$DF2EC442-B5B4-4F6A-A580-248095CC785D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"458ab467d1c5397109a383d0e5c939369d06a212","datavalue":{"value":{"entity-type":"item","numeric-id":3221403,"id":"Q3221403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$27A8BD79-6BFF-4CFC-80EC-DD5B03D4A4EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db1fabe871f96c24655853169e15cfa8cb749690","datavalue":{"value":{"entity-type":"item","numeric-id":1961709,"id":"Q1961709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$2B17D389-3B6B-49F5-BDED-B5CF677C2752","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adb9a1d4896e18f998666c6605fffb9d331dc6fc","datavalue":{"value":{"entity-type":"item","numeric-id":4375199,"id":"Q4375199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$2E66F9EC-BBCB-4E4C-B00B-069506931CC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc1be1343acc1e18378a260b5ef537373326f17c","datavalue":{"value":{"entity-type":"item","numeric-id":4364523,"id":"Q4364523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$BBF911C6-8834-4E46-ADEE-5EF5A61A4B0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a31384f6a5041124cd9e1741d2d8cc84eeffe20a","datavalue":{"value":{"entity-type":"item","numeric-id":4936123,"id":"Q4936123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$E13F505B-BE8F-4D32-B94A-A4801834960F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ed2ecec601f955b9bc942798454a6faa591b891","datavalue":{"value":{"entity-type":"item","numeric-id":4610330,"id":"Q4610330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$3BFF4205-6267-4DDB-B590-996031D6C6C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54bb8873ce1651399f10a1db5911162e96a0477f","datavalue":{"value":{"entity-type":"item","numeric-id":4645245,"id":"Q4645245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$23E03155-167C-4E7C-ADC7-BC8A4C427E91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6097cc60e6f31bf0c0a6c0f287889f4f5c97245","datavalue":{"value":{"entity-type":"item","numeric-id":4647498,"id":"Q4647498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$F347AE9F-E0EF-435A-BC63-E118E32DE55C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"687029087f5ee4053bd424cca81aac99b5667c42","datavalue":{"value":{"entity-type":"item","numeric-id":4936130,"id":"Q4936130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$3B21BAEC-E155-46CD-9882-F792683ECAFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8fd030717385500bfb13204e49473ce56dd0f9f","datavalue":{"value":{"entity-type":"item","numeric-id":1272615,"id":"Q1272615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1960430$DC083DBB-ACB0-4AFB-B29D-6E75DD577F0D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4934a407f1d8c884db587f42db154a949f7f59a1","datavalue":{"value":{"entity-type":"item","numeric-id":4790398,"id":"Q4790398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"985b1346d2f4bffe52daa9ccf8068f7cb53ed7b4","datavalue":{"value":{"amount":"+0.92191880941391","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":"Q1960430$FB7D1099-0C38-49DD-9948-A4EA44AEDEA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"823d50f5ac8a1a4a751660c59bfb6f1b45431044","datavalue":{"value":{"entity-type":"item","numeric-id":3129297,"id":"Q3129297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"21e1670fa4d72ad63ca4345730e60124ed232f72","datavalue":{"value":{"amount":"+0.917756199836731","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":"Q1960430$F2377844-5D5D-4330-9FAE-6F7E8F56723E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca00412e2d39fc69bcc4de993d33880967df5f7a","datavalue":{"value":{"entity-type":"item","numeric-id":4375199,"id":"Q4375199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea4a9292932c3b4bb29b3ef1d37e1e1b78a0d7f8","datavalue":{"value":{"amount":"+0.8393208980560303","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":"Q1960430$A7F3A19E-0645-494C-A787-CAD64F425E7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8f224617a51a1d4e4d508c109efa999bab49997","datavalue":{"value":{"entity-type":"item","numeric-id":4942001,"id":"Q4942001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f14ec6700db0e884e2126594151950593865e837","datavalue":{"value":{"amount":"+0.839320182800293","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":"Q1960430$C7CF364D-ACF2-4272-B592-CD75DA62B7BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"02e7f7f3e74a425dc7e6f7803f219525a1f125f9","datavalue":{"value":{"entity-type":"item","numeric-id":1854299,"id":"Q1854299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5180f6f2a179f3293068fdf7bd8ad386a32b7231","datavalue":{"value":{"amount":"+0.8124869465827942","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":"Q1960430$61A59888-AE70-446D-B0DC-C9C99497F7DF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1960430","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1960430"}}}}}