Re: [Hol-info] [isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic

> On 12 Mar 2018, at 19:12, Ken Kubota wrote: > > Thanks, this is what I expected. > > Concerning the Axiom of Choice (answering Mario's email, too), its use should > be expressed as a conditional of the form AC => THM (or as a hypothesis) and > not as an axiom in order

Re: [Hol-info] [isabelle] Mathematical Logics and Logical Frameworks

Ken, You should know about the Edinburgh Logical Framework (ELF), best implemented in the Twelf system. While ELF is a particular framework, there is tons of work about specification and programming in dependently typed frameworks. See e.g. many papers by Frank Pfenning, Amy Felty, Bob Harper,

Re: [Hol-info] HOL Help for Axiom.

Indeed. There is no need to distinguish axioms and axiom schemata (as Thomas said, oracles are not the latter). This is because of the INST and INST_TYPE rules of inference. In a system with schemata, instantiation (or matching) is the way you check whether or not you have an oracle, and you

Re: [Hol-info] HOL Help for Axiom.

Hi, just too clarify. Axioms and oracles are different things in HOL 4. In the context of HOL 4, an "oracle" usually refers to external proof tool which is trusted by HOL. Its results are "imported" using HOL's "oracle mechanism" (mk_oracle_thm and related). Oracles are __not__ axiom schemata.

[Hol-info] Mathematical Logics and Logical Frameworks

Dear Members of the Research Community, Finalizing my overview at http://www.owlofminerva.net/files/fom.pdf I would like to ask for major logics and logical frameworks not considered yet. The logical frameworks included now (as logical frameworks, not only object logics like Isabelle/HOL) are

[Hol-info] Axiom of Choice – Re: [isabelle] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic

Thanks, this is what I expected. Concerning the Axiom of Choice (answering Mario's email, too), its use should be expressed as a conditional of the form AC => THM (or as a hypothesis) and not as an axiom in order to make the appeal to it explicit. An example is the theorem in exercise X5308 in

Re: [Hol-info] HOL Help for Axiom.

There are 2 reasons for adding new axioms and axiom schemata (oracles): (1) To save the work for proving something provable or constructible (e.g.: one could assume the axioms for the real numbers instead of constructing the reals; although in this case, the library includes a construction of the

Re: [Hol-info] HOL Help for Axiom.

Dear Sana, it is easily possible to define own axioms and inference rules. However, it very easily leads to inconsistencies and is usually not advisable expect if you really know what you are doing. In most cases the definitional extension principles provided by HOL suffice and are much safer to

Re: [Hol-info] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic

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

[Hol-info] [Vardi-list] FLoC’18 Travel Support

FLoC’18 Travel Support Application Deadline: 18 May 2018 Applicants will be informed of decision by 1 June 2018 FLoC has some funds to provide travel grants of up to $1000 (USD) for student attendees of FLoC’18. Funds can be requested to cover airfare and lodging (registration fees and

[Hol-info] HOL Help for Axiom.

Hey. Hope you are fine. I am doing MS from National University of Science and Technology Islamabad. I need your help as i am working with HOL environment. Is it possible to define an *Inference Rule* or *Axiom* by myself? Kindly please guide me in this matter. Waiting for your kind response.

[Hol-info] SAS 2018: Call for Papers

- SAS 2018 25th Static Analysis Symposium Freiburg im Breisgau, Germany, August 29th-August 31st, 2018 http://staticanalysis.org/sas2018

[Hol-info] Second call for Papers: HVCS'18 - 5th Workshop on Horn Clauses for Verification and Synthesis

-- (apologies for multiple copies) Call for Papers 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS) Affiliated with ICLP at FLoC 2018 July 13, 2018 - Oxford, UK https://www.sci.unich.it/hcvs18/ Invited