Special Issue—Journal of Automated Reasoning
NONLINEAR REASONING
A variety of mature techniques for analyzing systems of linear inequalities
have been imported to the domain of automated reasoning. In contrast,
techniques for nonlinear functions are still being developed and examined.
Nonlinea
Special Issue—Journal of Automated Reasoning
NONLINEAR REASONING
A variety of mature techniques for analyzing systems of linear inequalities
have been imported to the domain of automated reasoning. In contrast,
techniques for nonlinear functions are still being developed and examined.
Nonlinea
Special Issue—Journal of Automated Reasoning
NONLINEAR REASONING
A variety of mature techniques for analyzing systems of linear inequalities
have been imported to the domain of automated reasoning. In contrast,
techniques for nonlinear functions are still being developed and examined.
Nonlinea
MetiTarski is an automatic theorem prover based on a combination of resolution
and computer algebra technology. It is designed to prove theorems involving
real-valued special functions such as ln, exp, sin, cos, arctan and sqrt. All
variables are assumed to range over the real numbers.
MetiTars
MetiTarski is an automatic theorem prover based on a combination of resolution
and computer algebra technology. It is designed to prove theorems involving
real-valued special functions such as ln, exp, sin, cos, arctan and sqrt. All
variables are assumed to range over the real numbers.
MetiTars
It can be downloaded from here:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6103
Larry Paulson
> On 8 Aug 2016, at 12:13, Ken Kubota wrote:
>
> Dear Members of the Research Community,
>
> As part of my efforts to try to understand the type system of Isabelle/HOL, I
> have gat
CALL FOR PAPERS
Special Issue On
MILESTONES IN INTERACTIVE THEOREM PROVING
Journal of Automated Reasoning
The past few decades have seen major achievements in interactive theorem
proving, such
ALEXANDRIA is a five-year ERC-funded project aimed at making interactive
theorem proving useful in mathematical research. The workplan includes pilot
studies to identify critical issues, library development and the implementation
of advanced search, perhaps using machine learning. Two mathematic
In response to recent requests, I have decided to make the full text of the
book ML for the Working Programmer available in PDF. It remains copyright
material and may be downloaded for personal use only, not for redistribution.
http://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html
Larry Paulson
The paper in question is Church (1940), which is available online (possibly
paywalled):
DOI: 10.2307/2266170
http://www.jstor.org/stable/2266170
On page 61 we see axiom 9 (description) and axiom 11 (choice).
Mike Gordon was clearly mistaken when he overlooked that Church's 1940 system
already
In 1983, using LCF_LSM, Mike verified his computer with the comment “The entire
specification and verification described here took several months, but this
includes some extending and debugging of LCF_LSM … it would take me two to four
weeks to do another similar exercise now. The complete proof r
On 2 Apr 2018, at 10:47,
wrote:
>
> I take it there's nothing in the CL area that used to be something like
> /usr/groups/hvg ?
I couldn't find it, though it may simply have moved somewhere. More worrying is
that none of the older links on this page work anymore:
http://www.cl.cam.ac.uk/res
Thanks for your kind answer, but I'm really looking for the opposite: to run
the classic old examples using the latest technology. It's a way of measuring
the progress of our field.
Larry
> On 4 Apr 2018, at 21:59, Chun Tian wrote:
>
> Hi,
>
> I didn't follow the entire discussions about “Go
I have just managed to locate Jeff Joyce's "Tamarack-2" files, which he
describes as slightly simplified compared with the original Gordon computer.
They are dated 1989 and the comments suggest that they are for HOL88. I guess
they will bring back the memories for some people. But it would proba
e harder to port, but I haven't
> looked...
> They could be added to HOL/examples in the HOL4 distribution -- if I find
> time to port them later (must leave it for now though..)
>
> On 5 April 2018 at 14:02, Lawrence Paulson <mailto:l...@cam.ac.uk>> wrote:
> It would
Somebody asked me, how do we represent the state of a sequential device in HOL?
And I am not quite sure. Mike himself wrote that it is simply about
incorporating time into the model, so that if we have a counter then we can
describe it by C(t+1) = C(t)+1, where C is its (visible) output and t
r
.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.pdf
>
> There is a sequential circuit example in that tech. report, which may help.
>
> Konrad.
>
>
> On Mon, Apr 23, 2018 at 9:09 AM, Lawrence Paulson wrote:
>> Somebody asked me, how do we represent the state of a sequential
Colleagues may be interested in my biographical article on Mike Gordon, whose
promotion of higher-order logic has had such a profound impact on our field.
https://arxiv.org/abs/1806.04002
Corrections welcome.
Larry Paulson
None of these attempts make any sense. In HOL and similar systems (including
Isabelle/HOL), it’s *impossible* to arrange for x/0 to be undefined in any
strong sense. Fortunately, it’s consistent and harmless to put x/0 = 0.
Larry Paulson
> On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourc
I sympathise with you here, as some mathematicians freak out at any mention of
division by zero. It’s not always easy for them to grasp what we are doing with
formal logic. You also need to bear in mind that mathematics texts are not
proved in any formal system, and in most cases, foundational m
In hardware, most devices are parameterised by a numerical bit width: buses,
counters, adders, registers, etc. So it seems obvious that people might have
tried to perform hardware verification using some form of dependent type
theory. Are there any particularly notable achievements along those l
MetiTarski is an automatic theorem prover based on a combination of
resolution and a decision procedure for the theory of real closed
fields. It is designed to prove theorems involving functions such as
log, exp, sin, cos and sqrt. MetiTarski is available to download; see
http://www.cl.cam.a
MetiTarski is an automatic theorem prover based on a combination of
resolution and a decision procedure for the theory of real closed
fields. It is designed to prove theorems involving functions such as
log, exp, sin, cos and sqrt. MetiTarski is available to download; see
http://www.cl.cam.a
MetiTarski is an automatic theorem prover based on a combination of
resolution and a decision procedure for the theory of real closed
fields. It is designed to prove theorems involving functions such as
log, exp, sin, cos and sqrt. MetiTarski is available to download; see
http://www.cl.cam.a
It is time to begin the process of selecting a host for ITP 2011, the
International Conference on Interactive Theorem Proving.
Following tradition from TPHOLs, the hosts of the previous conference (ITP
2010) are running the process. There are two phases: solicitation of bids and
voting. This m
MetiTarski is an automatic theorem prover based on a combination of resolution
and a decision procedure for the theory of real closed fields. It is designed
to prove theorems involving functions such as log, exp, sin, cos and sqrt.
MetiTarski is available to download; see
http://www.cl.cam.ac.u
p...@csl.sri.com, isabelle-us...@cl.cam.ac.uk, hol-info@lists.sourceforge.net,
om-annou...@openmath.org, theorem-prov...@ai.mit.edu
MetiTarski is an automatic theorem prover based on a combination of resolution
and a decision procedure for the theory of real closed fields. It is designed
to pro
MetiTarski is an automatic theorem prover based on a combination of resolution
and a decision procedure for the theory of real closed fields. It is designed
to prove theorems involving functions such as log, exp, sin, cos and sqrt.
MetiTarski is available to download; see
http://www.cl.cam.ac.u
MetiTarski is an automatic theorem prover based on a combination of resolution
and a decision procedure for the theory of real closed fields. It is designed
to prove theorems involving functions such as log, exp, sin, cos and sqrt.
MetiTarski is available to download; see
http://www.cl.cam.ac.u
MetiTarski is an automatic theorem prover based on a combination of resolution
and a decision procedure for the theory of real closed fields. It is designed
to prove theorems involving functions such as log, exp, sin, cos and sqrt.
MetiTarski is available to download; see
http://www.cl.cam.ac.u
This treatment of division by zero is fairly common in automated theorem
proving. I have written a discussion of the issues near the end of section
4.1.2 of my paper on MetiTarski:
http://www.cl.cam.ac.uk/~lp15/papers/Arith/MetiTarski-jar.pdf
The following paper is also relevant:
http://portal
MetiTarski is an automatic theorem prover based on a combination of resolution
and a decision procedure for the theory of real closed fields. It is designed
to prove theorems involving functions such as log, exp, sin, cos and sqrt.
MetiTarski is available to download; see
http://www.cl.cam.ac.u
MetiTarski is an automatic theorem prover based on a combination of resolution
and computer algebra technology. It is designed to prove theorems involving
real-valued special functions such as ln, exp, sin, cos, arctan and sqrt. All
variables are assumed to range over the real numbers.
MetiTars
MetiTarski is an automatic theorem prover based on a combination of resolution
and computer algebra technology. It is designed to prove theorems involving
real-valued special functions such as ln, exp, sin, cos, arctan and sqrt. All
variables are assumed to range over the real numbers.
MetiTars
MetiTarski is an automatic theorem prover based on a combination of resolution
and computer algebra technology. It is designed to prove theorems involving
real-valued special functions such as ln, exp, sin, cos, arctan and sqrt. All
variables are assumed to range over the real numbers.
MetiTars
MetiTarski is an automatic theorem prover based on a combination of resolution
and computer algebra technology. It is designed to prove theorems involving
real-valued special functions such as ln, exp, sin, cos, arctan and sqrt. All
variables are assumed to range over the real numbers.
MetiTars
36 matches
Mail list logo
