Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 11 of 11 for “"Proof Search"”.
-
Proof search issues in some non-classical logics
This thesis develops techniques and ideas on proof search. Proof search is used with one of two meanings. Proof search can be thought of either as the search for a yes/no answer to a query (theorem proving), or as the search for all proofs of a formula (proof enumeration). This thesis is an …
-
Nondeterminism and Language Design in Deep Inference
… with deep inference, in contrast to traditional proof-theoretic systems, inference rules can be applied at any depth inside logical expressions. Deep applicability of inference rules provides a rich combinatorial analysis of proofs. Deep inference also makes it possible to design deductive …
-
Language models for verifiable mathematical automation: Interaction, integration, and autoformalization
… it enables efficient verification of complex proofs, reduces the likelihood of errors in intricate calculations, allows non-experts to engage with mathematical concepts, and potentially facilitates the discovery of novel mathematical insights through machine-driven exploration. Traditionally, …
-
Compilation using correct-by-construction program synthesis
… code, reducing the extent of the guarantees that proof assistants and correct-by-construction program-derivation frameworks provide. We explore a novel approach to extracting and compiling embedded domain-specific languages developed in a proof assistant (Coq), showing how it allows us to extend …
-
A meta-language for functional verification
… between two activities: that of coordinating the search for simulation traces toward reaching verification closure, and that of coordinating the search for a proof within a theorem prover. The programmatic coordination of simulation is difficult with existing tools for digital circuit verification …
-
Relational compilation: Functional-to-imperative code generation for performance-critical applications
… shows how to recast program extraction as a proof-search problem to automatically derive correct-by-construction, high-performance code from shallowly embedded functional programs. It introduces a unifying framework, relational compilation, to capture and extend recent developments in program …
-
A Classification Approach for Automated Reasoning Systems--A Case Study in Graph Theory
… expressions of graph classes as a major proof method. The search is guided by case-split-based inferencing. Using the approach GC has generated proofs for many theorems such as "any two distinct cycles (closed paths) having a common edge e contain a cycle not traversing e", "if cycle C1 …
-
Higher-order proof translation
… the literature, but it is still an important research question. There are various logics and respective tools for carrying out formal developments, but practitioners still lament the difficulty of reliably exchanging mathematical data between tools. Writing proof-translation tools is hard. The …
-
TRACTABLE DEPTH-BOUNDED APPROXIMATIONS TO SOME PROPOSITIONAL LOGICS. TOWARDS MORE REALISTIC MODELS OF LOGICAL AGENTS.
… structural rule(s), can be used as a direct-proof and a refutation method, and is interesting independently of the approach in that it has an exponential speed-up on its tableau system counterpart. The latter given that we introduce a new class of examples which we prove to be hard for all …
-
Automated Multiparty Authorization in Open Distributed Systems
… control. While it is easy to verify a proof of authorization encoded in PeerAccess, the multilateral and distributed nature of multiparty authorization makes it difficult to construct such proofs. To facilitate distributed proof construction, we propose query routing rules to allow each …
-
User interaction widgets for interactive theorem proving
… of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof …