scholarly journals Experimenting with Theory Instantiation in Vampire

10.29007/pf85 ◽  
2020 ◽  
Author(s):  
Martin Riener
Keyword(s):  
Pure Theory ◽  
Smt Solver ◽  
Theory Reasoning

Theory instantiation tackles the problem of theory reasoning with quantifiers in Vam- pire using an SMT solver. In contrast to AVATAR modulo theories it works locally by instantiating a clause such that its pure theory part becomes inconsistent and can be deleted. We report on the challenges when adding instantiation for the theory of arrays.

Engineering Theories with Z3

10.29007/x7b4 ◽  
2018 ◽  
Author(s):  
Nikolaj Bjorner
Keyword(s):  
Satisfiability Modulo Theories ◽  
Smt Solver ◽  
Testing Tools ◽  
Software And Hardware ◽  
Design And Testing

Modern Satisfiability Modulo Theories (SMT)solvers are fundamental to many programanalysis, verification, design and testing tools. They are a goodfit for the domain of software and hardware engineering becausethey support many domains that are commonly used by the tools.The meaning of domains are captured by theories that can beaxiomatized or supported by efficient <i>theory solvers</i>.Nevertheless, not all domains are handled by all solvers andmany domains and theories will never be native to any solver.We here explore different theories that extend MicrosoftResearch's SMT solver Z3's basicsupport. Some can be directly encoded or axiomatized,others make use of user theory plug-ins.Plug-ins are a powerful way for tools to supply their custom domains.

A Reinterpretation of the Pure Theory of Exhaustion

1967 ◽  
Vol 75 (3) ◽  
pp. 274-286 ◽  
Author(s):  
Richard L. Gordon
Keyword(s):  
Pure Theory

Some Psychological Aspects of the Belief in Immortality

1919 ◽  
Vol 12 (3) ◽  
pp. 294-314
Author(s):  
James Bissett Pratt
Keyword(s):  
Related Question ◽  
Psychological Aspects ◽  
Pure Theory ◽  
The Future ◽  
The Individual

The individual's attitude toward the Determiner of Destiny, which is religion, has always an essentially practical coloring. It involves a belief, to be sure, but this belief is never a matter of pure theory; it bears a reference, more or less explicit, to the fate of the individual's values. Hence in nearly every religion which history has studied or anthropology discovered, the question of the future in store for the individual believer has been one of prime importance. The content of this belief is a question for the theologian and the historian of religion; the psychologist, however, may be able to throw some light on the related question why people believe, or fail to believe, in immortality at all. What, in short, are the psychological sources from which this belief springs, and what are the leading types of this belief?

scholarly journals Randomised testing of a microprocessor model using SMT-solver state generation

2016 ◽  
Vol 118 ◽  
pp. 60-76 ◽  
Author(s):  
Brian Campbell ◽  
Ian Stark
Keyword(s):  
Smt Solver ◽  
State Generation

Kelsen – Which Kelsen? A Reapplication of the Pure Theory to International Law

2009 ◽  
Vol 22 (2) ◽  
pp. 225-249 ◽  
Author(s):  
JÖRG KAMMERHOFER
Keyword(s):  
International Law ◽  
Legal Theory ◽  
Pure Theory ◽  
Municipal Law ◽  
Hans Kelsen ◽  
Theory Of Law ◽  
The Right ◽  
Relationship Of ◽  
The Relationship ◽  
Legal Theorist

AbstractHans Kelsen is known both as a legal theorist and as an international lawyer. This article shows that his theory of international law is an integral part of the Kelsenian Pure Theory of Law. Two areas of international law are analysed: first, Kelsen's coercive order paradigm and its relationship to the bellum iustum doctrine; second, the Kelsenian notion of the unity of all law vis-à-vis theories of the relationship of international and municipal law. In a second step, the results of Kelsenian general legal theory of the late period – as interpreted and developed by the present author – are reapplied to selected doctrines of international law. Thus is the coercive order paradigm resolved, the unity of law dissolved, and the UN Charter reinterpreted to show that the concretization of norms as positive international law cannot be unmade by a scholarship usurping the right to make law.

Melting curve for argon calculated from pure theory

1997 ◽  
Vol 224 (2-3) ◽  
pp. 253-261 ◽  
Author(s):  
Jan Solca ◽  
Anthony J. Dyson ◽  
Gerold Steinebrunner ◽  
Barbara Kirchner ◽  
Hanspeter Huber
Keyword(s):  
Melting Curve ◽  
Pure Theory

Reflections on the Pure Theory of Money of Mr. J. M. Keynes

Economica ◽  
1931 ◽  
pp. 270 ◽  
Author(s):  
F. A. von Hayek
Keyword(s):  
Pure Theory

Applying Test Data Generation Using SMT Solver to COBOL

2012 ◽  
Author(s):  
Yusuke Sasaki ◽  
Yoshiharu Maeda ◽  
Kenichi Kobayashi ◽  
Akihiko Matsuo
Keyword(s):  
Test Data ◽  
Test Data Generation ◽  
Data Generation ◽  
Smt Solver

The Pure Theory of Law.

1968 ◽  
Vol 18 (73) ◽  
pp. 377
Author(s):  
A. D. Woozley ◽  
Hans Kelsen ◽  
Max Knight
Keyword(s):  
Pure Theory ◽  
Theory Of Law
Sign in / Sign up

Export Citation Format

Share Document