{"entities":{"Q7361827":{"pageid":31521020,"ns":120,"title":"Item:Q7361827","lastrevid":105369701,"modified":"2026-10-07T13:38:38Z","type":"item","id":"Q7361827","labels":{"en":{"language":"en","value":"A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry Simple_Clause_Learning"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"25bd0e3224e731b1e624bd7a4b4e363f2149e4ba","datavalue":{"value":"https://isa-afp.org/entries/Simple_Clause_Learning.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361827$B9E8C056-C98C-43E7-8588-69E2A5557803","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"58f6a43946330a9b1c758022a21e1f99d75b5028","datavalue":{"value":{"time":"+2023-04-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361827$E4C8B769-CBA9-47DF-A4D2-0A7EA3649347","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"e5724ef8b4ec23cf8c7c0feafb67eeb84d745382","datavalue":{"value":"Martin Desharnais-Sch\u00e4fer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361827$DC03BB04-79D4-44D0-A3AF-E4D376FA06AA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2f6059d30da3e94ad38dd4bef86a4b52dbd9680f","datavalue":{"value":{"text":"A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361827$4015FD04-E61F-429B-A2A3-D287211DC87F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"667271c0fb1efe1b40d5f82f314b34ad86e9c0c6","datavalue":{"value":"This Isabelle/HOL formalization covers the unexecutable specification of Simple Clause Learning for first-order logic without equality: SCL(FOL). The main results are formal proofs of soundness, non-redundancy of learned clauses, termination, and refutational completeness. Compared to the unformalized version, the formalized calculus is simpler, a number of results were generalized, and the non-redundancy statement was strengthened. We found and corrected one bug in a previously published version of the SCL Backtrack rule. Compared to related formalizations, we introduce a new technique for showing termination based on non-redundant clause learning.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361827$9531FE46-A08C-48A5-87CD-A9D4406B8543","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab75901b0651ea9dcc948efb1ff1e44c7aa7ae8c","datavalue":{"value":{"entity-type":"item","numeric-id":6492736,"id":"Q6492736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$126290E2-7F62-4A16-971D-899E7A61B394","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d1db31f69f14e867729757963150857470e58a6","datavalue":{"value":{"entity-type":"item","numeric-id":2305416,"id":"Q2305416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$3270C811-2D44-4BB1-AD24-3C0FE6E8FC98","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$7787DE73-F1DC-41D1-A727-F8C682C2C456","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"6d228da4bce2fba997fec5a975b2ba853633b29e","datavalue":{"value":{"entity-type":"item","numeric-id":7361840,"id":"Q7361840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$DBA51708-5F99-4C4A-A796-A939A00CE688","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"618aa6266f7de671535c2b616862b142ebf9e094","datavalue":{"value":{"entity-type":"item","numeric-id":7361336,"id":"Q7361336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$C73DCDCC-B274-4E84-AB84-EE03169A008A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"505db3695b4bfab8c374d45d12041cac811b0acf","datavalue":{"value":{"entity-type":"item","numeric-id":7361268,"id":"Q7361268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$E8A91665-BC61-445E-B978-8DAD414E5F4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"249de87d0640153f3160c5acaab414f3ad84be18","datavalue":{"value":{"entity-type":"item","numeric-id":7361037,"id":"Q7361037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$304385E7-1380-44CC-9D7B-1ADE989D291D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"b9a61c696de92bdb09f875b4ad548670b0f0c015","datavalue":{"value":{"entity-type":"item","numeric-id":7361753,"id":"Q7361753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$C6BD8D5D-790B-4C0E-BE65-8CF4B5CFF6EA","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"fd4ac40fec1edeb460421a77e059cfe2df479821","datavalue":{"value":{"entity-type":"item","numeric-id":7360812,"id":"Q7360812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$A28F8A51-70CA-4524-9FE0-7D495191BDBF","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361827$40983F3A-E02C-4D12-9DEE-D2B95CCA025C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Formalization_of_the_SCL(FOL)_Calculus:_Simple_Clause_Learning_for_First-Order_Logic"}}}}}