Leopoldo Bertossi (Home Page)
School of Computer Science, Ottawa, Canada K1S 5B6.
Phone: (613)520-2600 x 1627; Fax: (613) 520 4334.
Title: Using Answer Set Programs to Specify Virtual Data Integration Systems under the LAV Appoach: Obtaining Consistent Query Answers
We show the design and specification of a virtual and relational data integration system under the local-as-view approach. We use answer set programs to specify the intended instances of the system and to deal with inconsistency wrt global integrity constraints.
We use XML and RuleML for representing metadata, like the mappings between local schemas and the global schema, and global integrity constraints. XQuery is used to retrieve relevant information for query planning. The system uses an extended inverse rules algorithm for computing certain answers. It provably works for monotone relational global queries. For query answering, evaluation engines for answer set programs on relational databases are used.
César Bautista Ramos (Home Page)
Facultad de Ciencias de la Computación
Benemérita Universidad Autónoma de Puebla
Title: A report on the lengths of proofs of Mendelson's formal theory L.
Following the metaproofs of the Mendelson's book "Introduction to Mathematical Logic" we calculate the proof lengths of some basic tautologies in the formal theory L using a formula for the growing length proof after the Deduction Theorem. Besides, a diagrammatical notation is introduced.