Constructive Second-Order Proofs in Logical Databases
Proceedings of the Tenth International Joint Conference on Artificial Intelligence. Reasoning. Pages 993-995.
Abstract
The constructive second-order proofs that we study are associated with inductive definitions on classes of finite s tructures , where each structure represents a database state. To an inductive definition of a predicate P on a class K corresponds a uniform proof of P i.e. a function which for each structure U defines a proof of P in U. These proofs use computations on sets and the finiteness of the structures in a fundamental way , and hence differ from fU"st-order proofs. We show the non-monotonicity of thi s calculus, and mention the constructivity of some of its intensional properties (time and space complexities) .
@inproceedings{ijcai1987p205,
title = {Constructive Second-Order Proofs in Logical Databases},
author = {de Rougemont, Michel},
booktitle = {Proceedings of the Tenth International Joint Conference on
Artificial Intelligence, {IJCAI-87}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {John McDermott},
pages = {993--995},
year = {1987},
note = {Reasoning},
url = {https://ijcai.org/proceedings/1987/205},
}
TY - CPAPER TI - Constructive Second-Order Proofs in Logical Databases AU - de Rougemont, Michel T2 - Proceedings of the Tenth International Joint Conference on Artificial Intelligence, IJCAI-87 PB - International Joint Conferences on Artificial Intelligence PY - 1987 SP - 993 EP - 995 UR - https://ijcai.org/proceedings/1987/205 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
