---
title: "Constructive Second-Order Proofs in Logical Databases"
authors:
  - "Michel de Rougemont"
doi: ""
url: "https://ijcai.org/proceedings/1987/205"
pdf: "https://ijcai.org/proceedings/1987/0205.pdf"
venue: "Proceedings of the Tenth International Joint Conference on Artificial Intelligence"
year: 1987
pages: "993-995"
track: "Reasoning"
keywords:
---

# Constructive Second-Order Proofs in Logical Databases

Michel de Rougemont

*Proceedings of the Tenth International Joint Conference on Artificial Intelligence*, 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) .