05695398

a

05695398 Nelson, Greg Reasoning about quantifiers by matching in the e-graph. Baader, Franz (ed.), Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40559-3/pbk). Lect. Notes Comput. Sci. 2741, 166 (2003). 2003 Berlin: Springer EN

doi:10.1007/b11829

Summary: The talk describes the method used for reasoning about quantifiers in the Simplify theorem-prover, which is the reasoning engine inside the Extended Static Checkers built for Java and for Modula-3 at the DEC/Compaq/HP Systems Research Center. The essence of the method is pattern-based heuristic instantiation.