{"entities":{"Q7361272":{"pageid":31519355,"ns":120,"title":"Item:Q7361272","lastrevid":105364448,"modified":"2026-10-07T13:35:20Z","type":"item","id":"Q7361272","labels":{"en":{"language":"en","value":"Auto2 Prover"}},"descriptions":{"en":{"language":"en","value":"AFP entry Auto2_HOL"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0e1d744798539ac800ca862fcb208c78d82e85ac","datavalue":{"value":"https://isa-afp.org/entries/Auto2_HOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361272$79B07761-1AAE-4C59-8A21-46D816627531","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"dd5f23ee54392c85eac5a5d27f88a008ee6a7846","datavalue":{"value":{"time":"+2018-11-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":"Q7361272$AFE7B1D1-3CB6-4149-BE8E-635D55EEC6EA","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"01aade34926865f306029ac4b82b2852e9efa5b5","datavalue":{"value":"Bohua Zhan","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361272$2EEA5EF8-2ED8-4EAE-AF04-C9216D7AE924","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c558a4241f075cfe66058a87d3770df54e3b96c6","datavalue":{"value":{"text":"Auto2 Prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361272$634DDE6D-147C-44AC-A13D-6604A189B73C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6cc7b2ac30bf5f5e1728542fbdc99a6e6b4ddefe","datavalue":{"value":"Auto2 is a saturation-based heuristic prover for higher-order logic, implemented as a tactic in Isabelle. This entry contains the instantiation of auto2 for Isabelle/HOL, along with two basic examples: solutions to some of the Pelletier\u2019s problems, and elementary number theory of primes.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361272$D95E203B-D812-4663-A8A6-2669F46D01E8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a1ce762817aa67ba84d34579fd3b9060a2c653","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361272$BF45E13F-7EBB-4D9F-9868-87161D74CDCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5587664e371fa7cdb52e3b1329f22cf9fcff022","datavalue":{"value":{"entity-type":"item","numeric-id":1101242,"id":"Q1101242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361272$87EA7240-0B58-4E48-975C-86AC165915EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a914c4e44dde41b17e5fb1fd3ebe0fef3dbf648","datavalue":{"value":{"entity-type":"item","numeric-id":2829278,"id":"Q2829278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361272$68ABD6A9-8117-4300-ADC1-D938EE29E3EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da5b389dccb05fe2dd61d661d50f9146c3a64d94","datavalue":{"value":{"entity-type":"item","numeric-id":2324204,"id":"Q2324204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361272$D364633D-B933-4876-A346-23ED5FF3FA48","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":"Q7361272$BDBB8329-9145-4451-8295-A33C8C67A9D1","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361272$F6BD3CD8-8961-4440-8022-971A67166D86","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":"Q7361272$F47E4C24-D8FB-4A41-9E40-124C4EAA9674","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Auto2 Prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Auto2_Prover"}}}}}