Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userConjectures, Tests and Proofs: An Overview of Theory Exploration
105
0
0.0
(
0
)
Added by
EPTCS
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Authors
Moa Johansson
Ask ChatGPT about the research
No Arabic abstract
A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory exploration system called QuickSpec, which is able to automatically discover interesting conjectures about a given set of functions. QuickSpec works by interleaving term generation with random testing to form candidate conjectures. This is made tractable by starting from small sizes and ensuring that only terms that are irreducible with respect to already discovered conjectures are considered. QuickSpec has been successfully applied to generate lemmas for automated inductive theorem proving as well as to generate specifications of functional programs. We give an overview of typical use-cases of QuickSpec, as well as demonstrating how to easily connect it to a theorem prover of the users choice.
rate research
Read More
The search for increased trustworthiness of SAT solvers is very active and uses various methods. Some of these methods obtain a proof from the provers then check it, normally by replicating the search based on the proofs information. Because the certification process involves another nontrivial proof search, the trust we can place in it is decreased. Some attempts to amend this use certifiers which have been verified by proofs assistants such as Isabelle/HOL and Coq. Our approach is different because it is based on an extremely simplified certifier. This certifier enjoys a very high level of trust but is very inefficient. In this paper, we experiment with this approach and conclude that by placing some restrictions on the formats, one can mostly eliminate the need for search and in principle, can certify proofs of arbitrary size.
Gurevich (1988) conjectured that there is no logic for $textsf{P}$ or for $textsf{NP}cap textsf{coNP}$. For the latter complexity class, he also showed that the existence of a logic would imply that $textsf{NP} cap textsf{coNP}$ has a complete problem under polynomial time reductions. We show that there is an oracle with respect to which $textsf P$ does have a logic and $textsf P etextsf{NP}$. We also show that a logic for $textsf{NP} cap textsf{coNP}$ follows from the existence of a complete problem and a further assumption about canonical labelling. For intersection classes $Sigma^p_n cap Pi^p_n$ higher in the polynomial hierarchy, the existence of a logic is equivalent to the existence of complete problems.
We improve and refine a method for certifying that the values sizes computed by an imperative program will be bounded by polynomials in the programs inputs sizes. Our work tames the non-determinism of the original analysis, and offers an innovative way of completing the analysis when a non-polynomial growth is found. We furthermore enrich the analyzed language by adding function definitions and calls, allowing to compose the analysis of different libraries and offering generally more modularity. The implementation of our improved method, discussed in a tool paper (https://hal.archives-ouvertes.fr/hal-03269121), also required to reason about the efficiency of some of the needed operations on the matrices produced by the analysis. It is our hope that this work will enable and facilitate static analysis of source code to guarantee its correctness with respect to resource usages.
Orthogonality is a discipline of programming that in a syntactic manner guarantees determinism of functional specifications. Essentially, orthogonality avoids, on the one side, the inherent ambiguity of non determinism, prohibiting the existence of different rules that specify the same function and that may apply simultaneously (non-ambiguity), and, on the other side, it eliminates the possibility of occurrence of repetitions of variables in the left-hand side of these rules (left linearity). In the theory of term rewriting systems (TRSs) determinism is captured by the well-known property of confluence, that basically states that whenever different computations or simplifications from a term are possible, the computed answers should coincide. Although the proofs are technically elaborated, confluence is well-known to be a consequence of orthogonality. Thus, orthogonality is an important mathematical discipline intrinsic to the specification of recursive functions that is naturally applied in functional programming and specification. Starting from a formalization of the theory of TRSs in the proof assistant PVS, this work describes how confluence of orthogonal TRSs has been formalized, based on axiomatizations of properties of rules, positions and substitutions involved in parallel steps of reduction, in this proof assistant. Proofs for some similar but restricted properties such as the property of confluence of non-ambiguous and (left and right) linear TRSs have been fully formalized.
Embodied computer vision considers perception for robots in novel, unstructured environments. Of particular importance is the embodied visual exploration problem: how might a robot equipped with a camera scope out a new environment? Despite the progress thus far, many basic questions pertinent to this problem remain unanswered: (i) What does it mean for an agent to explore its environment well? (ii) Which methods work well, and under which assumptions and environmental settings? (iii) Where do current approaches fall short, and where might future work seek to improve? Seeking answers to these questions, we first present a taxonomy for existing visual exploration algorithms and create a standard framework for benchmarking them. We then perform a thorough empirical study of the four state-of-the-art paradigms using the proposed framework with two photorealistic simulated 3D environments, a state-of-the-art exploration architecture, and diverse evaluation metrics. Our experimental results offer insights and suggest new performance metrics and baselines for future work in visual exploration. Code, models and data are publicly available: https://github.com/facebookresearch/exploring_exploration
suggested questions
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
