scholarly journals Set of Support for Theory Reasoning

10.29007/ndjg ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Practical Reasoning ◽  
Negative Impact ◽  
Theorem Prover ◽  
Suggested Approach ◽  
Theorem Provers ◽  
Support Strategy ◽  
Explicit Theory ◽  
Ordering Constraints ◽  
Theory Reasoning ◽  
Limited Reasoning

This paper describes initial experiments using the set of support strategy to improve how a saturation-based theorem prover performs theory reasoning with explicit theory axioms. When dealing with theories such as arithmetic, modern automated theorem provers often resort to adding explicit theory axioms, for example, x+y = y+x. Reasoning with such axioms can be explosive. However, little has been done to explore methods that mitigate the negative impact of theory axioms on saturation-based reasoning. The set of support strategy requires that all inferences involve a premise with an ancestor in a so-called set of support,initially taken to be a subset of the input clauses, usually those corresponding to the goal. This leads to completely goal orientated reasoning but is incomplete for practical reasoning (e.g. in the presence of ordering constraints). The idea of this paper is to apply the set of support strategy to theory axioms only, and then to explore the effect of allowing some limited reasoning within this set. The suggested approach is implemented and evaluated within the VAMPIRE theorem prover.

scholarly journals Leo-III Version 1.1 (System description)

10.29007/grmx ◽  
2018 ◽  
Author(s):  
Christoph Benzmüller ◽  
Alexander Steen ◽  
Max Wisniewski
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
System Description ◽  
Agent Based ◽  
First Order ◽  
Theorem Provers ◽  
Automated Theorem Prover ◽  
Ordering Constraints

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external first-order theorem provers.Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III's underlying calculus, survey implementation details and give examples of use.

scholarly journals AN EFFICIENT CHAOS-BASED OPTIMIZATION ALGORITHM APPROACH FOR CRYPTOGRAPHY

2012 ◽  
pp. 75-79
Author(s):  
RASHI VOHRA ◽  
BRAJESH PATEL
Keyword(s):  
Genetic Algorithm ◽  
Optimization Algorithm ◽  
Negative Impact ◽  
Chaotic Map ◽  
Pseudorandom Sequence ◽  
Secure Communications ◽  
Security Threats ◽  
Suggested Approach ◽  
Novel Approach ◽  
Algorithm Operation

The utmost negative impact of advancement of technology is an exponential increase in security threats, due to which tremendous demand for effective electronic security is increasing importantly. The principles of any security mechanism are confidentiality, authentication, integrity, non-repudiation, access control and availability. Cryptography is an essential aspect for secure communications. Many chaotic cryptosystem has been developed, as a result of the interesting relationship between the two field chaos and cryptography phenomenological behavior. In this paper, an overview of cryptography, optimization algorithm and chaos theory is provided and a novel approach for encryption and decryption based on chaos and optimization algorithms is discussed. In this article, the basic idea is to encrypt and decrypt the information using the concept of genetic algorithm with the pseudorandom sequence further used as a key in genetic algorithm operation for encryption: which is generated by application of chaotic map. This attempt result in good desirable cryptographic properties as a change in key will produce undesired result in receiver side. The suggested approach complements standard, algorithmic procedures, providing security solutions with novel features.

scholarly journals Deep Network Guided Proof Search

10.29007/8mwc ◽  
2018 ◽  
Author(s):  
Sarah Loos ◽  
Geoffrey Irving ◽  
Christian Szegedy ◽  
Cezary Kaliszyk
Keyword(s):  
Deep Learning ◽  
Program Analysis ◽  
Network Models ◽  
Theorem Prover ◽  
Neural Network Models ◽  
Two Phase ◽  
First Order ◽  
Proof Search ◽  
System Verification ◽  
Theory Reasoning

Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playing the game of Go.Automated first-order theorem provers can aid in the formalization and verification of mathematical theorems and play a crucial role in program analysis, theory reasoning, security, interpolation, and system verification.Here we suggest deep learning based guidance in the proof search of the theorem prover E. We train and compare several deep neural network models on the traces of existing ATP proofs of Mizar statements and use them to select processed clauses during proof search. We give experimental evidence that with a hybrid, two-phase approach, deep learning based guidance can significantly reduce the average number of proof search steps while increasing the number of theorems proved.Using a few proof guidance strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.

CALL FOR PAPERS Journal of Functional Programming Special Issue on Theorem Provers and Functional Programming

1997 ◽  
Vol 7 (1) ◽  
pp. 125-126
Author(s):  
Tom Melham
Keyword(s):  
Interface Design ◽  
Functional Programming ◽  
Type Systems ◽  
Theory And Practice ◽  
Theorem Prover ◽  
Functional Languages ◽  
Special Issue ◽  
Theorem Provers ◽  
Problems And Solutions ◽  
Submission Deadline

A special issue of the Journal of Functional Programming will be devoted to the use of functional programming in theorem proving. The submission deadline is 31 August 1997.The histories of theorem provers and functional languages have been deeply intertwined since the advent of Lisp. A notable example is the ML family of languages, which are named for the meta language devised for the LCF theorem prover, and which provide both the implementation platform and interaction facilities for numerous later systems (such as Coq, HOL, Isabelle, NuPrl). Other examples include Lisp (as used for ACL2, PVS, Nqthm) and Haskell (as used for Veritas).This special issue is devoted to the theory and practice of using functional languages to implement theorem provers and using theorem provers to reason about functional languages. Topics of interest include, but are not limited to:– architecture of theorem prover implementations– interface design in the functional context– limits of the LCF methodology– impact of host language features– type systems– lazy vs strict languages– imperative (impure) features– performance problems and solutions– problems of scale– special implementation techniques– term representations (e.g. de Bruijn vs name carrying vs BDDs)– limitations of current functional languages– mechanised theories of functional programming

scholarly journals Checkable Proofs for First-Order Theorem Proving

10.29007/s6d1 ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Theorem Proving ◽  
Critical Mass ◽  
Current Situation ◽  
Boolean Satisfiability ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Theorem Provers ◽  
Interactive Theorem Provers ◽  
Theory Reasoning

Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),we argue that a similar goal of having unified automatically checkable proofs should be soughtby the developers of automated first-order theorem provers (ATPs). This would not onlyhelp to further increase assurance about the correctness of prover results,but would also be indispensable for tools which rely on ATPs,such as ``hammers'' employed within interactive theorem provers.The current situation, represented by the TSTP format is unsatisfactory,because this format does not have a standardised semantics and thus cannot be checked automatically.Providing such semantics, however, is a challenging endeavour. One would ideallylike to have a proof format which covers only-satisfiability-preserving operations such as Skolemisationand is versatile enough to encompass various proving methods (i.e. not just superposition)or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.Going beyond pure first-order logic to theory reasoning in the style of SMT orbeyond proofs to certification of satisfiability are further interesting challenges.Although several projects have already provided partial solutions in this direction,we would like to use the opportunity of ARCADE to further promote the idea andgather critical mass needed for its satisfactory realisation.

scholarly journals Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry

10.29007/pqh1 ◽  
2018 ◽  
Author(s):  
Josef Urban ◽  
Robert Veroff
Keyword(s):  
State Of The Art ◽  
Theorem Provers ◽  
Theory Reasoning

We describe our experiments with several state-of-the-art automated theorem provers on the problems in Tarskian Geometry created by Beeson and Wos. In comparison to the manually-guided Otter proofs by Beeson and Wos, we can solve a large number of problems fully automatically, in particular thanks to the recent large-theory reasoning methods.

scholarly journals Improving ENIGMA-style Clause Selection while Learning From History

2021 ◽  
pp. 543-561
Author(s):  
Martin Suda
Keyword(s):  
Neural Network ◽  
Real Time ◽  
Theorem Prover ◽  
Central Idea ◽  
Theorem Provers ◽  
Recursive Neural Network ◽  
Time Evaluation ◽  
Automatic Theorem ◽  
Learning From History

AbstractWe re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recognizing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We propose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a recursive neural network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The automatic theorem prover Vampire guided by the network achieves a 41 % improvement on a relevant subset of SMT-LIB in a real time evaluation.

scholarly journals GridTPT: a distributed platform for Theorem Prover Testing

10.29007/hk8w ◽  
2018 ◽  
Author(s):  
Thomas Bouton ◽  
Diego Caminha ◽  
David Déharbe ◽  
Pascal Fontaine
Keyword(s):  
Open Source ◽  
Future Development ◽  
Theorem Prover ◽  
Complex Task ◽  
Smt Solver ◽  
Requirement Specification ◽  
Open Source Tool ◽  
Theorem Provers ◽  
Distributed Platform ◽  
Implementation Resources

Programming provers is a complex task; completeness or even soundness may often be broken by apparently harmless bugs. A good testing platform can contribute in detecting problems early and helping development. This paper presents GridTPT, the distributed platform for testing the verit SMT solver. Its features are fairly standard, but it allows to easily distribute the task in a cluster.We plan to make this platform available as an open source tool for the community of developers of automated theorem provers. This presentation to PAAR'2010 will provide the opportunity to discuss the need for such a tool and the necessary features in a broader context. We would like to extract a requirement specification from this discussion, that would be useful to get dedicated implementation resources for distribution, maintenance and future development of GridTPT.

Constraint-based reasoning on declarative process execution with the logics workbench

2015 ◽  
Vol 21 (3) ◽  
pp. 586-609 ◽  
Author(s):  
Vitus Lam
Keyword(s):  
Practical Reasoning ◽  
Process Modelling ◽  
Process Models ◽  
Theorem Prover ◽  
Business Rules ◽  
Business Rule ◽  
Content Type ◽  
Formal Framework ◽  
Execution Trace ◽  
New Business

Purpose – An integral part of declarative process modelling is to guarantee that the execution of a declarative workflow is compliant with the respective business rules. The purpose of this paper is to establish a formal framework for representing business rules and determining whether any business rules are violated during the executions of declarative process models. Design/methodology/approach – In the approach, a business rule is phrased in terms of restricted English that is related to a constraint template. Linear temporal logic (LTL) is employed as a formalism for defining the set of constraint templates. By exploiting the theorem-proving feature of the Logics Workbench (LWB), business rule violations are then detected in an automatic manner. Findings – This study explored the viability of encoding: first, process executions by means of LTL and second, business rules in terms of restricted English that built upon pattern-oriented templates and LTL. The LWB was used for carrying out temporal reasoning through automated techniques. The applicability of the formal verification approach was exemplified by a case study concerning supply chain management. The findings showed that practical reasoning could be achieved by combining declarative process modelling, restricted English, pattern-oriented templates, LTL and LWB. Originality/value – First, new business rule templates are proposed; second, business rules are expressed in restricted English instead of graphical constructs; third, both finite execution trace and business rules are grounded in LTL. There is no need to deal with the semantic differences between different formalisms; and finally, the theorem prover LWB is used for the conformance checking of a finite execution trace against business rules.

STRATEGY PARALLELISM IN AUTOMATED THEOREM PROVING

1999 ◽  
Vol 13 (02) ◽  
pp. 219-245 ◽  
Author(s):  
ANDREAS WOLF ◽  
REINHOLD LETZ
Keyword(s):  
Theorem Proving ◽  
Experimental Evaluation ◽  
Automated Theorem Proving ◽  
Search Strategies ◽  
Theorem Prover ◽  
Strategy Selection ◽  
Theorem Provers ◽  
Initial Strategy ◽  
Basic Concepts ◽  
Run Time

Automated theorem provers use search strategies. Unfortunately, there is no unique strategy which is uniformly successful on all problems. This motivates us to apply different strategies in parallel, in a competitive manner. In this paper, we discuss properties, problems, and perspectives of strategy parallelism in theorem proving. We develop basic concepts like the complementarity and the overlap value of strategy sets. Some of the problems such as initial strategy selection and run-time strategy exchange are discussed in more detail. The paper also contains the description of an implementation of a strategy parallel theorem prover (p-SETHEO) and an experimental evaluation.

Sign in / Sign up

Export Citation Format

Share Document