Re: Date and McGoveran comments on view updating 'problem'

On Dec 11, 5:37 am, paul c <toledobythe..._at_oohay.ac> wrote:
> Another question I have is whether anybody here knows whether Prover9
> depends on a lattice formulation, or could it be applied using the TTM
> A-algebra instead?

Prover9 is a general purpose theorem prover, so it can accommodate any algebra. It has it's own limitations, of course. As the number of operations&axioms grows up, you'll be quickly frustrated with Prover9 (or any other automatic tool for that matter) inability to deduce useful properties. This is why keeping algebra simple is paramount.

Regarding algebraic version of TTM aka "A"lgebra, you'll have to overcome technical difficulty of projection being not really pure algebraic operation. FWIW, the posting
http://groups.google.com/group/comp.databases.theory/browse_thread/thread/de5c7c301cd141f2/25ecbb6d37945d41?hl=en#25ecbb6d37945d41 describes how D&D "A"lgebra fits into a "bi-lattice" system of one unary operation, 4 binary operations, and 4 constants. The symmetry of this system is skewed in a peculiar way, but it remains to be seen if the inclusion of the "*" and "+" adds any more power compared to RL described in
http://arxiv.org/ftp/arxiv/papers/0807/0807.3795.pdf Received on Thu Dec 11 2008 - 20:11:47 CET