{"entities":{"Q1868166":{"pageid":1878908,"ns":120,"title":"Item:Q1868166","lastrevid":48085792,"modified":"2026-01-03T14:25:42Z","type":"item","id":"Q1868166","labels":{"en":{"language":"en","value":"Comparing approaches to resolution based higher-order theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1901268"}},"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":"Q1868166$C682B307-4D20-4CCD-A86D-E00787521C59","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c6d9861f7ae84bd8302bbda3914fa70cf252e131","datavalue":{"value":{"text":"Comparing approaches to resolution based higher-order theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1868166$10DE9494-0BE7-4B29-8BD9-04EC2AFB71E8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f1e98bea4fd93a23b94fd58213e92c25cacb10dd","datavalue":{"value":"1020.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868166$0CF6C244-4DB1-4657-9E18-886F1BA88F3F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"258739f9b04ce75ad7f9946e3fc6bcc495d0e8c6","datavalue":{"value":"10.1023/A:1020840027781","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868166$5B038726-1850-40AE-AC3C-E33AFE79FB6E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a525f7cd8b191ac2b9090383b0dabde3689f4ff2","datavalue":{"value":{"entity-type":"item","numeric-id":287280,"id":"Q287280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868166$F61927B0-D3F1-459E-8DB0-E28BEB351BFA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"28921346d64a666ce2dd47540df2f388e07634f5","datavalue":{"value":{"entity-type":"item","numeric-id":162813,"id":"Q162813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868166$9387D0BA-849F-4D9B-BD86-83D14BBE6157","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ae7235402c0b574ed2e2213feb9e21452b645cac","datavalue":{"value":{"time":"+2003-04-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1868166$C9C4BB25-EFF0-46D3-B610-43F9B356A865","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fb864ca271547e10863523b4cb4f10c484fa6fde","datavalue":{"value":"Four approaches to resolution-based higher-order theorem proving are investigated: Andrews' higher-order resolution approach; Huet's constrained resolution approach; higher-order E-resolution; and extensional higher-order resolution. The author focuses on Henkin completeness and full extensionality.   The paper demonstrates that simply adding extensionality axioms to the search space increases the amount of blind search. Higher-order E-unification and R-resolution improves the situation but it does still not provide a general solution. Extensional higher-order resolution is the sole studied approach that can completely avoid the extensionality axioms.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868166$5E92B760-AC4F-4542-834F-44151C028469","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868166$AEC486BA-CB1D-4C03-A071-D66E4CE76983","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868166$EF8D8466-547F-4C23-83D3-4DCA15BF40E1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4e912b378816f0e7024794c9f6013b86ae8c73d9","datavalue":{"value":"1901268","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868166$02294056-48BF-476B-93C9-2DD31BFEC19C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868166$AFD19609-ADF9-47C1-AF23-A6DC3BB98EFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3b739adea7cc6595553157e408987428d6e06a8","datavalue":{"value":"higher-order resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868166$9527DE9C-FB18-4CCF-9A16-BEFF86DFE460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6484ea3f3814c7fb8866474cbfc658164e9e61d","datavalue":{"value":"resolution-based higher-order theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868166$CE129B3F-0A17-4EE1-BE4A-EE317BFF6FE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a9b404d5273aea460c76feaed1e6d6c90337c789","datavalue":{"value":"Henkin completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868166$403EE9E9-14FD-4EC8-A1C0-5E64B11409E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"56e514529cb78b604756585a701df73620563a6e","datavalue":{"value":"full extensionality","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868166$0253997D-BA02-43F5-B5DA-20C83AAF0F7D","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"05f3dff3edc7d97b14af7ecb326f488fb3fee31b","datavalue":{"value":{"entity-type":"item","numeric-id":583186,"id":"Q583186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868166$7282EBB7-3614-496D-83C0-594674C2273C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c40cf9a35904f638a7cabef2bc178bad46391f7","datavalue":{"value":{"entity-type":"item","numeric-id":13717,"id":"Q13717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868166$F786CEEC-90A1-46FF-A839-8C4B7271A851","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"42d0367ffc4d2b82e6fb2192cfde6351c1daa402","datavalue":{"value":{"entity-type":"item","numeric-id":31432,"id":"Q31432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868166$686D8552-53CB-48AE-BAA8-31CF29078A13","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":"Q1868166$6015A963-4DA3-4A10-86A2-7DBE4546C5A9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1e24d147815426ba327fed8e2eff2c18be0132e1","datavalue":{"value":"https://doi.org/10.1023/a:1020840027781","type":"string"},"datatype":"url"},"type":"statement","id":"Q1868166$435D3943-3F2D-43E4-9EEE-5F526245EF12","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b90fe88e4760f8db6ac992e79fbc91506dd1c256","datavalue":{"value":"W2021219068","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868166$690A780A-5CD8-4D0B-B3DC-FC5A9D3BE8CD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cf76f67380c4606cdc24ddf91ef319c5e832666","datavalue":{"value":{"entity-type":"item","numeric-id":4249891,"id":"Q4249891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97db7d9ddd5baf4ee2f58c72354f6d7cc4b75b7f","datavalue":{"value":{"amount":"+0.8278165459632874","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":"Q1868166$10610EAF-FC1D-40CE-9A77-7FE6E2E248A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7fed98c364da768f7151867a2161bfd994bdea7e","datavalue":{"value":{"entity-type":"item","numeric-id":6488561,"id":"Q6488561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97db7d9ddd5baf4ee2f58c72354f6d7cc4b75b7f","datavalue":{"value":{"amount":"+0.8278165459632874","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":"Q1868166$28261C87-5281-4097-8056-612BFB0289FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00eeadb8ca107f43b52703f930458c0a9c22a34d","datavalue":{"value":{"entity-type":"item","numeric-id":4263170,"id":"Q4263170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fad1710e99e43c9cc8c17d3486b093a39796fe78","datavalue":{"value":{"amount":"+0.8079949021339417","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":"Q1868166$A5FB1E10-85EC-4AEE-9AB5-16952BE4CF88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0ec97b8481b3a0b1d3747ab1cfe1014f767440b","datavalue":{"value":{"entity-type":"item","numeric-id":4524794,"id":"Q4524794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3833eb4a4885a2c103ff0dbf761bfb8283a4350d","datavalue":{"value":{"amount":"+0.7603034377098083","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":"Q1868166$5776227A-FA1F-4A87-B741-C2E5964F613A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c23c68568ccdab2f69246a1a1cd7cff5d21c092f","datavalue":{"value":{"entity-type":"item","numeric-id":5966632,"id":"Q5966632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3833eb4a4885a2c103ff0dbf761bfb8283a4350d","datavalue":{"value":{"amount":"+0.7603034377098083","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":"Q1868166$63BED300-BE15-40DE-B3CB-4EA80BF402B7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1868166","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1868166"}}}}}