Skip to Content.
Sympa Menu

coq-club - [Coq-Club] An invitation: implementing a variant of situation calculus

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] An invitation: implementing a variant of situation calculus


chronological Thread 
  • From: Qiang Liu <lqiangecnu AT gmail.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] An invitation: implementing a variant of situation calculus
  • Date: Mon, 21 Dec 2009 20:57:55 +0800
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=X4mIXDxnnp7NSdznC46bG0XL0fUY1tAojNRtfS4bwXCOI4PF/FJqA5m7k3qhnjKn1Q 7Mr6hmuHlNyrG448rTyaJ8n8UwhWycXMMsIclAp52L0g7n3CmvyuEuayh9kKvfzVBN+m 79VMNHxjHTSPobGIyIA1tzXMSY/Xml0YPbvn8=


hi, everyone, i am planning to implement a variant of situation calculus in Coq. My ultimate goal is to give syntactical restriction on BAT(Basic Action Theory), so some newly proposed First-Order Model Checking algorithms will be guaranteed to terminate. Anyone interested in this topic ? 



Archive powered by MhonArc 2.6.16.

Top of Page