The DCEC* is a quantified modal logic that builds upon on the first-order Event Calculus (EC). EC has been used quite successfully in modelling a wide range of phenomena, from those that are purely physical to narratives expressed in natural-language stories. The EC is also a natural platform to capture natural-language semantics, especially that of tense. However, EC has a shortcoming: it is fully extensional, and hence, has no support for capturing intensional concepts such as knowledge and belief without introducing unsoundness or inconsistencies. For example, consider the possibility of modeling changing beliefs with fluents. We can posit a “belief” fluent belief(a,f) which says whether an agent a believes another fluent f. This approach quickly leads to serious problems, as one can substitute co-referring terms into the belief term, which leads to either unsoundness or an inconsistency. One can try to overcome this using more complex schemes of belief encoding in FOL, but they all seem to fail. A more detailed discussion of such schemes and how they fail can be found in the publications listed on this page.

A more detailed overview is available at: http://www.cs.rpi.edu/~govinn/dcec.pdf

DOWNLOADS

We have several tools in development for working with the DCEC*:

• TALOS: A DCEC* prover based on SPASS. This is a web-based API so that you can use the DCEC* prover anywhere with minimal installation.
  • Page to request API Key: https://prover.cogsci.rpi.edu/DCEC_PROVER/keyGenerator.php
  • Prover interface: https://prover.cogsci.rpi.edu/DCEC_PROVER/
  • Example file for calling prover in Python
  • Full source (in case you want to build a local copy of the prover yourself): https://github.com/JamesPane-Joyce?tab=repositories
• Shadow Prover: A DCEC* prover written in LISP which uses the SNARK theorem prover. Current version available at https://github.com/sirmarcis/DCECProver. (Naveen Sundar Govindarajulu / Anders Maraviglia)
• GF-Based Parser: A real-time parser based on the Grammatical Framework that converts Controlled English sentences into DCEC* formulae
• SC Parser: A parser based on the Stanford Core NLP Libraries that converts English sentences into DCEC* formulae (coming soon)
• Dataset: A dataset consisting of DCEC* formulae, their English sentence equivalents, and a partial graph showing that some of the formulae in this database can be proven from the others (in development)
• Uncertainty Ensemble: Uses a Gödel-encoding of Kolmogorovian axioms of probability and a Chisholm-ian 9-valued logic of epistemic strength. Includes the Necessity and Possibility operators of quantified K/T/4/5 modal logic. (Selmer Bringsjord) (in development)
• DPLs: Based on Denotational Proof Languages (DPLs), inspired by Konstantine Arkoudas’s “Athena” system. Based on fluid logics and category theory, and by analogy related to model finders. Tied to Joshua Taylor’s PhD dissertation. (Joshua Taylor) (in development)

PUBLICATIONS

BRINGSJORD, S. & GOVINDARAJULU, N. Deontic cognitive event calculus (formal specification). Available at http://kryten.mm.rpi.edu/PRICAI_w_sequentcalc_041709.pdf, 2013.
BRINGSJORD, S. & GOVINDARAJULU, N. Nuclear deterrence and the logic of deliberative mindreading. Gognitive Systems Research 28 (June 2014), 20– 43.
GOVINDARAJULU, N. S., LICATO, J., AND BRINGSJORD, S. Small steps toward hypercomputation via infinitary machine proof verification and proof generation. In Unconventional computation and natural computation – 12th international conference (UCNC 2013) (2013), G. Mauri, A. Dennunzio, L. Manzoni, and A. E. Porreca, Eds., pp. 102–112.

PRIMARY PERSONNEL

• Selmer Bringsjord
• Naveen Sundar Govindarajulu

PRIMARY CONTACT – Rikhiya Ghosh