coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Getting the immediate consequences from applying some theorem or tactic, Coq for knowledge base completion and forward chaining?

From: Alex Meyer <alex153 AT outlook.lv>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Getting the immediate consequences from applying some theorem or tactic, Coq for knowledge base completion and forward chaining?
Date: Sun, 8 Sep 2019 14:00:34 +0000
Accept-language: lv-LV, en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=2jrLI+bQRCOIFovvwuRiPBf/f8jh4KCgSOyu+YkKb6o=; b=WhRPkgc034P1kjD++p0lbj+JPXX5SNu0760r70dtNsDfixGSKo/dpF2Iq1lhskgkviIRGwq+I04zUiD6ze9LbJnwd/9NgMdDPt02KbUh50U/mE4/6Kc5EVWRFYDBF6neBMOcuzfA0J4XuYVw55ipfGSiZB55aRD4B1jIzW4loquS+X1JhGIzv1M9SjBAVh5fQYBaZi04qmObfrA3JzKlxdoY8o/wLow02PvhdksVATL4Y0nvz/I5inBvUpZ4wnny3TuvgFolPLDbSR2SXmdxRSV5b6THuFdNOR81ho/LnU0ftdLV72502ptLXw1y6/u7e3gdMyU33hrxi2pPT/eayQ==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=jYkPwaP5A6a/iiW2nkAD0iFCRi3G2h9LpBseU4XUHlw5FWeRz/9EXT7B1PElRbbFAPK3pPH/TjR0pfKlHiWtTH7KuwMEuv0JlXo8qeJ6TtB45XXhcNDlGXPLD2OYti+Bpqif8h6UOBauEQsYQpXC2EUJj3WBa+DqMVfMVHdkMwfBmIz98YolQb+2gqxAgQu/7LGxqCX86nUA3O+subnNJGM9c/NEmkP5IM0ieP227jB0eSWabj9fgYopUtgTCXxij1oga3NJxU/gi0ZUWQUePL736LCi7OfsVjUpus/NFBOSELyIlMtEfmXrR4VP6GOHnc9Vo5VhHDG4qDp2dqClaw==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alex153 AT outlook.lv; spf=Pass smtp.mailfrom=alex153 AT outlook.lv; spf=Pass smtp.helo=postmaster AT EUR02-VE1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:m9JirBfUs/zg4f38eQbvMmZAlGMj4u6mDksu8pMizoh2WeGdxcS8bR7h7PlgxGXEQZ/co6odzbaP6ea5CTBLvs7JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MQu6oR/MusQVjoZuJaQ8xgfUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vpwJxzZPIYI+bN/RxYqzScMgASmZdQspcTTBNDp+iY4YJEuEPPfxYr474p1YWsRa+ARejBezywTFPmHD33bM10/48GgzBxgMgG8wBsXvJoNj1OqofSue1zLTUzTXHaPNW3jT95JLMchA/uPyBW697f8TWyUkqDQzFj1OQpJT+PzOJzOsCr2ub7+1+Ve2xkW4npQVxoj+hx8s2lobJgYcVxkjf9SVl2ok1I9O4SElhYdG5CpdfqTyVN5ZwT8g/QG9ooD43x7IatZKheCUG1o4ryh/bZvCdcYWE/wrvVOiPLjp7mH5ofbeyiAyu/kS91OLxU9W73VJUoSVZl9TBtWwB2wDW58WDV/Rw+Fqq1yyV2ADJ8O5EJFg5larFJJ4lxb49jpUdvkrfECPqhkn6laCZeEo59uSx7OToeavpqoWbN49plgHxKaMumtG5AeslKAQOR3Kb+eOg1LL94UL5XLRKjvowkqXDt5DaONgbpqq+Aw9S0YYv8QqwDzCj0NgAnHkHKkxKeA6fgoXmJ13COvT1Aemlj1mtlDpn3fLLMqD5DpXINHfDkbPhfbhn605bzQo+1cpQ55ZKBbAOPf7+WkH8ucffDh8kLwy0x+HnCNJ+1o8EXWKPHLeVMLnOvl+Q+uIvP+6MaZcJtzb6Mvgp/uLhjXskmVAGZqSpxpsWaHWgHvt8OUmZYHzsgs0AEWgQpAY+Qvbq2xW+VmsZbHGrGqk4+zsTCYS8DI6FSJrnyOiK2z7+FZlLbEhHDEqNGDHmbdPXde0LbXe7JsJx2hkJRLW7A9so0Ry+7VKh4716Mu7T/S5esYy1h4s93PHaiRxnrW88NM+ayWzYFzglzFNNfCc/2eVEmWI4z16C1aZihPkBT45U+u9NVQA5c5rCnbUjVoLCHznZd9LMc26IB9WrBTZtEYAc/uVWOQNDNozniRrOmS23H7USirqHQoQu9b7R1GTwIMA7zGva0K4mjB8tRc4dbDT61J46zBDaAsvyq2vcj7yjLP5O2zPR8GCEziyKohMAXQ==

Hello!

Coq, of course, is proof assistant and one declared lemma and tries to find goal. That is fine. Enormous amount of formal knowledge (formalization of notions, concepts, rules and axioms, formally proved theorems and so on) is gathered in such way in Coq language and format. But is it possible to use all this wealth for forward reasoning, for calculation?

Simple questions: is it possible to use Coq as calculator, e.g. to declare that x=4+5 and then try to find x? is it possible to calculate _immediate_ consequences for some set of axioms&proved theorems and some valid rules, tactics? Of course, the complete set of consequences if infinite and contains lot of garbage, but my question is about the immediate consequences.

The method described in the article "Guding inference in Relational Reinforcement Learning" http://cll.stanford.edu/~langley/papers/icarus.rrl.ilp05.pdf is the reason why I am asking for such forward reasoning feature in Coq: external software can decide on the set of interesting premises (subset of already proved theorems and assumed facts) and on the promising theorems/rules/tactics and may all this information forward to the Coq and then Coq can make immedate consequences out, one step for forward reasoning. And then it is up to the external system to estimate the usefulness of acquired/deduced knowledge and to go forward (possibly useing reinforcement learning approach - neural or symbolic/relational).

That is why the forward reasoning feature would be of importance for the Coq and it should be enabled somehow? Is it possible? It would be very sad to translate all the results of Coq formalization into other systems for doing forward reasoning (besides, I don't know any such system that can do it).

I asked this question in Stackexchange https://stackoverflow.com/questions/57836193/how-to-use-coq-as-calculator-or-as-forward-chaining-rule-engine-sequence-applica/57836284#57836284 and got good suggestions, but it would be nice to hear more, maybe about the future prospects as well abd about the consciseness of such approach.

Thanks, Alex

[Coq-Club] Getting the immediate consequences from applying some theorem or tactic, Coq for knowledge base completion and forward chaining?, Alex Meyer, 09/08/2019