Abstract
It is shown in this paper a way of representing deductive systems using the situation calculus. The situation calculus is a family of first order languages with induction that allows the specification of evolving worlds and reasoning about them and has found a number of applications in AI. A method for the representation of formulae and of proofs is presented in which the induction axiom on states is used to represent structural induction on formulae and proofs. This paper's formalizations are relevant for the purpose of meta reasoning and of automated or manual deduction in the context of situation calculus specifications. An example proof is given for the fact that no deductive system is complete for arbitrary situation calculus specifications (an expectable result). © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Sáez, P. (2005). Deductive systems’ representation and an incompleteness result in the situation calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3789 LNAI, pp. 119–131). Springer Verlag. https://doi.org/10.1007/11579427_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
