scholarly journals The Isabelle/Naproche Natural Language Proof Assistant

2021 ◽  
pp. 614-624
Author(s):  
Adrian De Lon ◽  
Peter Koepke ◽  
Anton Lorenzen ◽  
Adrian Marti ◽  
Marcel Schütz ◽  
...  
Keyword(s):  
Natural Language ◽  
Proof Assistant ◽  
Current Version ◽  
Proof Checking ◽  
Controlled Natural Language ◽  
Mathematical Texts

Abstract"Image missing" is an emerging natural proof assistant that accepts input in the controlled natural language ForTheL. "Image missing" is included in the current version of the Isabelle/PIDE which allows comfortable editing and asynchronous proof-checking of ForTheL texts. The dialect of ForTheL can be typeset by "Image missing" into documents that approximate the language and appearance of ordinary mathematical texts.

scholarly journals The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts

2010 ◽  
pp. 170-186 ◽  
Author(s):  
Marcos Cramer ◽  
Bernhard Fisseni ◽  
Peter Koepke ◽  
Daniel Kühlwein ◽  
Bernhard Schröder ◽  
...  
Keyword(s):  
Natural Language ◽  
Proof Checking ◽  
Controlled Natural Language ◽  
Mathematical Texts

scholarly journals Towards an Automated Model-Based Test Generation Approach from Controlled Natural Language Specifications Written in Arabic

2021 ◽  
Author(s):  
Moez Krichen ◽  
Seifeddine Mechti
Keyword(s):  
Natural Language ◽  
Test Generation ◽  
Arabic Language ◽  
Test Cases ◽  
New Model ◽  
Controlled Natural Language ◽  
Model Based ◽  
Case Grammar ◽  
Model Based Testing ◽  
Testing Approach

<div>We propose a new model-based testing approach which takes as input a set of requirements described in Arabic Controlled Natural Language (CNL) which is a subset of the Arabic language generated by a specific grammar. The semantics of the considered requirements is defined using the Case Grammar Theory (CTG). The requirements are translated into Transition Relations which serve as an input for test cases generation tools.</div>

scholarly journals Towards an Automated Model-Based Test Generation Approach from Controlled Natural Language Specifications Written in Arabic

2021 ◽  
Author(s):  
Moez Krichen ◽  
Seifeddine Mechti
Keyword(s):  
Natural Language ◽  
Test Generation ◽  
Arabic Language ◽  
Test Cases ◽  
New Model ◽  
Controlled Natural Language ◽  
Model Based ◽  
Case Grammar ◽  
Model Based Testing ◽  
Testing Approach

<div>We propose a new model-based testing approach which takes as input a set of requirements described in Arabic Controlled Natural Language (CNL) which is a subset of the Arabic language generated by a specific grammar. The semantics of the considered requirements is defined using the Case Grammar Theory (CTG). The requirements are translated into Transition Relations which serve as an input for test cases generation tools.</div>

scholarly journals Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant

2021 ◽  
pp. 450-467
Author(s):  
Hans-Jörg Schurr ◽  
Mathias Fleury ◽  
Martin Desharnais
Keyword(s):  
Success Rate ◽  
Failure Rate ◽  
Proof Assistant ◽  
Proof Checking ◽  
Smt Solver ◽  
Fine Grained ◽  
Simple Rules ◽  
Detailed Evaluation ◽  
Reconstruction Time

AbstractWe present a fast and reliable reconstruction of proofs generated by the SMT solver veriT in Isabelle. The fine-grained proof format makes the reconstruction simple and efficient. For typical proof steps, such as arithmetic reasoning and skolemization, our reconstruction can avoid expensive search. By skipping proof steps that are irrelevant for Isabelle, the performance of proof checking is improved. Our method increases the success rate of Sledgehammer by halving the failure rate and reduces the checking time by 13%. We provide a detailed evaluation of the reconstruction time for each rule. The runtime is influenced by both simple rules that appear very often and common complex rules.

Sign in / Sign up

Export Citation Format

Share Document