Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

25

LPAR
2012
Springer

favoriteEmaildiscussreport

318views Automated Reasoning» more LPAR 2012»

Querying Proofs

11 years 12 months ago

Querying Proofs

Download ti.arc.nasa.gov

We motivate and introduce a query language PrQL designed for inspecting machine representations of proofs. PrQL natively supports hiproofs which express proof structure using hierarchical nested labelled trees. The core language presented in this paper is locally structured, with queries built using recursion and patterns over proof structure and rule names. We deﬁne the syntax and semantics of locally structured queries, demonstrate their power, and sketch some implementation experiments.

David Aspinall, Ewen Denney, Christoph Lüth

Real-time Traffic

Automated Reasoning | LPAR 2012 | Machine Representations | Proof Structure | Syntax And Semantics |

claim paper

Related Content

» Small PCPs with Low Query Complexity

» Formal Proof Reconciling Correctness and Understanding

» A Simple Proof for the TuringCompleteness of XSLT and XQuery

» Confidentialitypreserving distributed proofs of conjunctive queries

» On Finding an InferenceProof Complete Database for Controlled Query Evaluation

» ProofInfused Streams Enabling Authentication of Sliding Window Queries On Streams

» Query Execution Assurance for Outsourced Databases

» Negative Ordered HyperResolution as a Proof Procedure for Disjunctive Logic Programming

» Short PCPs with Polylog Query Complexity

Post Info
More Details (n/a)

Added	25 Apr 2012
Updated	25 Apr 2012
Type	Journal
Year	2012
Where	LPAR
Authors	David Aspinall, Ewen Denney, Christoph Lüth

Comments (0)