A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning.
Fabio AlessiAlberto CiaffaglionePietro Di GianantonioFurio HonsellMarina LenisaPublished in: LFMTP@LICS (2019)
Keyphrases
- logical framework
- reasoning tasks
- inference rules
- belief revision
- linear logic
- possibilistic logic
- epistemic logic
- higher order logic
- logic programming
- object oriented
- theorem prover
- coalition logic
- automated reasoning
- formal methods
- default reasoning
- probabilistic reasoning
- situation calculus
- decision problems
- model checking