The Coq mailing list

[like <12like34xiongmao AT 163.com>]

Hi Adam Chlipala: 
> 
> This is certainly a fairly unusual choice in Coq formalization.  
> However, I'd be careful about thinking of this as meaning that you have 
> an unusual problem domain that demands unusual encoding.  I would 
> recommend thinking hard about how to formalize your logic without axioms.



The logic I want to embed is called PPTL（propositional projection temporal
logic）. The paper is  "A complete proof system for propositional projection
temporal logic (2012)". Duan Z, Zhang N, Koutny M. You can find it in 
http://www.sciencedirect.com/science/article/pii/S030439751200062  . Thanks 
for
your help.
                                                                          
                                                                   like