Justifying proofs using memo tables | Zendy

Abhik Roychoudhury | Zendy; C. R. Ramakrishnan | Zendy; I. V. Ramakrishnan | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Justifying proofs using memo tables

Author(s) -

Abhik Roychoudhury,

C. R. Ramakrishnan,

I. V. Ramakrishnan

Publication year - 2000

Publication title -

citeseer x (the pennsylvania state university)

Language(s) - English

Resource type - Conference proceedings

ISBN - 1-58113-265-4

DOI - 10.1145/351268.351290

Subject(s) - computer science , mathematical proof , programming language , construct (python library) , abstraction , proof theory , theoretical computer science , logic programming , table (database) , overhead (engineering) , mathematics , database , geometry , philosophy , epistemology

Tableau-based proof systems can be elegantly specified and directly executed by a tabled Logic Programming (LP) system. Our experience with the XMC model checker shows that such an encoding can be used to search for the existence of a proof very efficiently. However, the users of a tableau system are often interested in getting sufficient evidence (in terms of the tableau proof rules) on why a proof does or does not exist. In this paper, we address the problem of constructing such an evidence...

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research