Computing Transivity Tables: A Challenge For Automated Theorem Provers

摘要: Implementations of Allen's interval-based temporal logic and a recently developed simulation system for reasoning about space time, both require the use transitivity tables. Although strategies exist to construct such tables, proofs which underly entries in table are tedious do some cases difficult secure. Often proof is only obtained via lemmas; moreover, finding models satisfiable sets dyadic relations theory introduces its own difficulties. This paper presents problems. Any automated theorem prover can effectively generate tables would mark significant progress proving.