论文部分内容阅读
时态逻辑不可递归公理化的性质，造成它的公理化系统和证明论方法不适于时态查询语言的建模．这使得时态逻辑无法利用公理化系统的良好性质及相关证明论方法对时态数据库的推理和查询做更为严谨和细致地刻画．因此寻找时态逻辑的替代者，以公理化的方式对时态查询语言做句法和语义的分析是必要的．考虑的2个主要工具是作为句法分析工具的以Lambek演算为核心的范畴语法系统，和作为语义分析工具的类型演算λ－演算．这主要是基于类型论的演算特点、SQL语句与陈述句的相似性、Lambek演算和λ－演算的公理化与证明论方法，及它们作为句法