In the development of logic-based formal theories, traditional approaches which rely on first-order classical logic suffer from a number of limitations such as semi-decidability, closed-world assumption, difficulty to cope with partial knowledge, etc. Many solutions have been proposed for these topics, but difficulties and uncertainties remain, even in the latest papers. In order to address these problems, we suggest a new proof-theoretical perspective within a fragment of constructive type theory for reasoning about actions with contexts. The basic structure of the theory are Dependent Record Types (DRTs) which model contexts, actions and effects through a simple and natural representation. DRTs have a higher expressive power and are able to express partial knowledge and dynamic reasoning while assuming an Open World Assumption.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com