{"entities":{"Q7361855":{"pageid":31521104,"ns":120,"title":"Item:Q7361855","lastrevid":105369497,"modified":"2026-10-07T13:38:00Z","type":"item","id":"Q7361855","labels":{"en":{"language":"en","value":"Practical Algebraic Calculus Checker"}},"descriptions":{"en":{"language":"en","value":"AFP entry PAC_Checker"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"453bb331c29b839cae5c39c97d189a537d923c2c","datavalue":{"value":"https://isa-afp.org/entries/PAC_Checker.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361855$F7380E8C-F4F5-41AA-9464-53CEFD03FD6F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2a92243b7f71031e288e3329b3f00a17d48f45e0","datavalue":{"value":{"time":"+2020-08-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361855$3E9484F0-0500-499E-9426-84783DDB6BC4","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"945ab20dca3d165b4fc3dec98847d7b03a5dc77f","datavalue":{"value":"Mathias Fleury","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361855$02AD7515-4F42-44C1-BBAB-3EF26888C914","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"c263f88ee30f69aa53faa3b733e98df2357becc4","datavalue":{"value":"Daniela Kaufmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361855$7A775945-84FE-42F5-8675-29658969A14F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"50d0bfde941a9cc32898a83006e5720db6161a7e","datavalue":{"value":{"text":"Practical Algebraic Calculus Checker","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361855$749A35EF-AC00-4B52-BA26-2D809FB8987B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cc57fdeff3be09014920f8494c50773e2c9d8566","datavalue":{"value":"Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus (PAC). In this development, we present the verified checker Past\u00e8que that is obtained by synthesis via the Refinement Framework. This is the formalization going with our FMCAD'20 tool presentation.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361855$54344D06-3B67-4D75-B450-D7BE23361851","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":"Q7361855$40C15013-F7D9-498C-96D8-9D839848938D","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"8f0f13c41ff97fc90cd117120ced19e3dd24a1b3","datavalue":{"value":{"entity-type":"item","numeric-id":7361305,"id":"Q7361305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361855$D314184E-0226-47F2-B690-AF9183905B0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"3083b28cc1bd9860f5bb551df5db6c97e7a4c0c4","datavalue":{"value":{"entity-type":"item","numeric-id":7361593,"id":"Q7361593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361855$5EF60199-7F99-4220-B09C-C57ED089424A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"6df1e1600a3acc40d1b0a9c9cf7cbc177462ddf9","datavalue":{"value":{"entity-type":"item","numeric-id":7361373,"id":"Q7361373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361855$A928E8BD-530B-4B9D-A4BC-EC6A97A68E6D","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"1157f6239d5752bb0ad1cee836272bd46c6bf40f","datavalue":{"value":{"entity-type":"item","numeric-id":7360772,"id":"Q7360772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361855$92F32B69-5CAF-4346-B302-F5E840A15E95","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":"Q7361855$EA07E201-B2FD-450F-B444-061F3C2603A2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Practical Algebraic Calculus Checker","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Practical_Algebraic_Calculus_Checker"}}}}}