The Coq Proof Script Visualiser (coq-psv)

• URL: http://arxiv.org/abs/2101.07761v1
• Date: Fri, 15 Jan 2021 08:52:31 GMT
• Title: The Coq Proof Script Visualiser (coq-psv)
• Authors: Mario Frank
• Abstract summary: This tool supports both education and review processes as all proof steps can be visualised. In contrast to the usual approach of visualising proofs as hypertext or markdown documents, the generated files can be easily printed.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: In this work, we present a visualisation tool that is able to process Coq proof scripts and generate a table representation of the contained proofs as $\LaTeX$ or PDF files. This tool has the aim to support both education and review processes as all proof steps can be visualised. Thus, there is no need to use Coq in order to review proofs or use them as examples in teaching. In contrast to the usual approach of visualising proofs as hypertext or markdown documents, the generated files can be easily printed.

Related papers

• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but it is expensive. Recent research has used machine learning to automatically synthesize proofs, reducing verification effort, but these tools are able to prove only a fraction of the desired software properties. We introduce Cobblestone, a new proof-synthesis approach that improves on the state of the art by taking advantage of partial progress in proof synthesis attempts.
  arXiv  Detail & Related papers  (2024-10-25T19:25:00Z)
• CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
  This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data.
  arXiv  Detail & Related papers  (2024-05-07T12:50:28Z)
• Visually Guided Generative Text-Layout Pre-training for Document Intelligence [51.09853181377696]
  We propose visually guided generative text-pre-training, named ViTLP. Given a document image, the model optimize hierarchical language and layout modeling objectives to generate the interleaved text and layout sequence. ViTLP can function as a native OCR model to localize and recognize texts of document images.
  arXiv  Detail & Related papers  (2024-03-25T08:00:43Z)
• Towards Automatic Transformations of Coq Proof Scripts [0.0]
  We present a framework to carry out a posteriori script transformations. These transformations are meant to be applied as an automated post-processing step, once the proof has been completed. We apply our tool to various Coq proof scripts, including some from the GeoCoq library.
  arXiv  Detail & Related papers  (2024-01-22T12:48:34Z)
• Text-Conditioned Resampler For Long Form Video Understanding [94.81955667020867]
  We present a text-conditioned video resampler (TCR) module that uses a pre-trained visual encoder and large language model (LLM) TCR can process more than 100 frames at a time with plain attention and without optimised implementations.
  arXiv  Detail & Related papers  (2023-12-19T06:42:47Z)
• Advancing Visual Grounding with Scene Knowledge: Benchmark and Method [74.72663425217522]
  Visual grounding (VG) aims to establish fine-grained alignment between vision and language. Most existing VG datasets are constructed using simple description texts. We propose a novel benchmark of underlineScene underlineKnowledge-guided underlineVisual underlineGrounding.
  arXiv  Detail & Related papers  (2023-07-21T13:06:02Z)
• Precise Zero-Shot Dense Retrieval without Relevance Labels [60.457378374671656]
  Hypothetical Document Embeddings(HyDE) is a zero-shot dense retrieval system. We show that HyDE significantly outperforms the state-of-the-art unsupervised dense retriever Contriever.
  arXiv  Detail & Related papers  (2022-12-20T18:09:52Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)
• Proof Blocks: Autogradable Scaffolding Activities for Learning to Write Proofs [0.4588028371034407]
  Proof Blocks is a software tool which enables students to write proofs by dragging and dropping prewritten proof lines into the correct order. These proofs can be graded completely automatically, enabling students to receive rapid feedback on how they are doing with their proofs. When constructing a problem, the instructor specifies the dependency graph of the lines of the proof, so that any correct arrangement of the lines can receive full credit.
  arXiv  Detail & Related papers  (2021-06-07T17:03:58Z)
• Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge [0.0]
  We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant. Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps. Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
  arXiv  Detail & Related papers  (2020-12-20T18:15:12Z)
• Evidence-Aware Inferential Text Generation with Vector Quantised Variational AutoEncoder [104.25716317141321]
  We propose an approach that automatically finds evidence for an event from a large text corpus, and leverages the evidence to guide the generation of inferential texts. Our approach provides state-of-the-art performance on both Event2Mind and ATOMIC datasets.
  arXiv  Detail & Related papers  (2020-06-15T02:59:52Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.