{"entities":{"Q4649555":{"pageid":6679136,"ns":120,"title":"Item:Q4649555","lastrevid":82273562,"modified":"2026-05-06T20:30:44Z","type":"item","id":"Q4649555","labels":{"en":{"language":"en","value":"Herbrand-confluence for cut elimination in classical first order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6109842"}},"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":"Q4649555$4242EF83-0837-415F-B83B-4AE385115B8A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dc7de3fdc3f76f29c40f080e24ba1cc2d26cbf15","datavalue":{"value":"1252.03123","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4649555$1167275E-F8AA-4E09-A6E7-061963E93B20","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ac16dcce5f3df8b1bf1087e5a90fdae80fa7a2e5","datavalue":{"value":{"entity-type":"item","numeric-id":402112,"id":"Q402112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4649555$E85D50C4-A7F4-498A-81C7-AB491629C0EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"47e9ac37086b3bbcbf1225cf6575ab3c2b196e0c","datavalue":{"value":{"entity-type":"item","numeric-id":714730,"id":"Q714730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4649555$819613B9-B9B1-4878-801E-6EBB3714A099","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2f3aa46d2f66375aad8f9f235cf6aa2da570e73e","datavalue":{"value":{"time":"+2012-11-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4649555$187DB506-2D01-4444-8625-F461C59F2E50","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4649555$D234DFA4-FD73-43CC-9488-403102A11786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4649555$A648B064-67AF-4535-A08C-E7C2D6C22DEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c270fb88a62fde738bd530246c5ba57a005a4efd","datavalue":{"value":"03D05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4649555$51F7B3EB-80DA-4076-97A0-D3D98DAE1FCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4649555$1199EDE3-AA68-4848-9C1F-8B1AB93EEACD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"926f0b3f42934adda7c258a970bcff051435c515","datavalue":{"value":"6109842","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4649555$F190110F-0315-4E3C-947B-2201A12B33E5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4649555$A0FC6129-8E49-44BC-824B-BAFE71583772","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4649555$1C6B066D-DCC0-4A1A-ACA0-66350BCAC103","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a1a2bad4593dfa53b9bdf6d73901a5fbf0b67c8a","datavalue":{"value":"tree languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q4649555$83F51E72-6112-4037-9EEB-AF887E477A54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q4649555$F254E22E-1B46-4135-B3B6-243291DFDB49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"284b76663a91b98251e130360fa617d9ecaf8ab5","datavalue":{"value":"semantics of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q4649555$5D6FB5F2-CF89-4FF7-BB3B-E21EEA34D4B5","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":"Q4649555$F06567F8-82E2-42E4-AC49-97A60F3BC4BD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b2b048adf69273192bbfb87f0a4ae7cca6225aa0","datavalue":{"value":"https://inria.hal.science/hal-00759228","type":"string"},"datatype":"url"},"type":"statement","id":"Q4649555$5D92EF3F-4F80-4C4E-B963-81678F297248","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5b64af60a01a95102d45c634ea0d4ea9761c3c97","datavalue":{"value":"W2240567774","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4649555$F8F0C488-F0CE-4C5F-8054-D21FABE12D36","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c376067e144b7a674347d634d78c25676c8b26db","datavalue":{"value":{"text":"Herbrand-Confluence for Cut Elimination in Classical First Order Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4649555$BA1E00D7-4B4E-4473-AA0E-A9649A4EEF09","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f2359d37bcc9a33a0a53b10e73e5532be90a5031","datavalue":{"value":"10.4230/LIPICS.CSL.2012.320","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4649555$743C2464-6BC7-4725-874A-A77D7DC5140B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78e05ea5b7d7260ca535be85672730a3681c9e77","datavalue":{"value":{"entity-type":"item","numeric-id":2871477,"id":"Q2871477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8eb66b6ffd675d83432ae547f989f701fad02ec3","datavalue":{"value":{"amount":"+0.988875150680542","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":"Q4649555$86F83811-B3AB-4D8D-B388-E77E5D360CD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c76f77ea149ac341d5cf455fcbd6b85ee4566ec","datavalue":{"value":{"entity-type":"item","numeric-id":1854335,"id":"Q1854335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7b97f42ae707e27def14e47ddbebd4bb55672f1","datavalue":{"value":{"amount":"+0.8840768933296204","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":"Q4649555$C2314FD3-8A65-49B1-AC8C-BF652B2A8EAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec290a654ce54a07fa3d9cb8e5571225b93f307a","datavalue":{"value":{"entity-type":"item","numeric-id":5221602,"id":"Q5221602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb5deaf80d0eb32b9d128cccb2d0da75757c5ca0","datavalue":{"value":{"amount":"+0.8319805860519409","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":"Q4649555$BC8BD3D5-E230-4742-858C-4F5B3C31607C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4c44e02d3ba1fb404b3e82a6a5ef631beffe17f4","datavalue":{"value":{"entity-type":"item","numeric-id":2946689,"id":"Q2946689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3ed7cd563807bba4989fe94b46ce20f43a44a11","datavalue":{"value":{"amount":"+0.8098088502883911","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":"Q4649555$F74F5CD9-9B75-4E5D-B427-BA17EAF027A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6316d4020e0fb67c0e9dd75f11b02cf7043dfe01","datavalue":{"value":{"entity-type":"item","numeric-id":3083141,"id":"Q3083141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e1b477eff359f980f73bdf039a48285420c1a64","datavalue":{"value":{"amount":"+0.8025703430175781","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":"Q4649555$172938A5-A70A-406B-B340-DE1AB6F201EC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Herbrand-confluence for cut elimination in classical first order logic","badges":[]}}}}}