[open-axiom-devel] 1.4.x branch and pending 1.4.0 release

Hi,

We are nearing the overdue release of OpenAxiom 1.4.0, hopefully by the
end of the weekend.  I create the 1.4.x branch for that purpose.
To check it out

   svn co https://open-axiom.svn.sf.net/snvroot/open-axiom/1.4.x oa-1.4.x

There have been lot of changes since 1.3.0.  I would like to get
OpenAxiom-1.4.0 out of the door soon.

The Windows platform build is moving toward a new GUI interface.  At the
moment, we have a basic GUI interface that still relies on the ASCII art 
display.  Graphics is not yet provided, but it is #1 item for 1.4.1.

The one thing that remains is the merging of Arthur's browser/server
interface to mainline.

Please test the 1.4.x branch and let me know of build problems or other
outstanding issues.  

(I'll be attending ISSAC 2011 in San Jose for those of you who would be
there.  There will be a poster and a paper presentation on on-going
automatic parallelization work based on OpenAxiom.)

Thanks,

-- Gaby

Re: [open-axiom-devel] Re: computation framework

Martin Baker <ax87438@...> writes:

[...]

| In other words they seem to be saying that the addition of either Law
| of the excluded middle or Double negation elimination have the same
| effect of converting intuitionistic logic to classical logic.

If you want to support intuitionistic logic, you cannot simplify
double negation.  See my comment in the definition of simplifyOneStep
in the package PropositionalFormulaFunctions1

  http://svn.open-axiom.org/viewvc/open-axiom/trunk/src/algebra/boolean.spad.pamphlet?revision=2022&view=markup

-- Gaby

------------------------------------------------------------------------------
EditLive Enterprise is the world's most technically advanced content
authoring tool. Experience the power of Track Changes, Inline Image
Editing and ensure content is compliant with Accessibility Checking.
http://p.sf.net/sfu/ephox-dev2dev

Re: [open-axiom-devel] computation framework

Waldek Hebisch <hebisch@...> writes:

[...]

| To say this differently: --T = T but there are x such that
| --x ~= x.

Yep.  See simplifyOneStep in

   http://svn.open-axiom.org/viewvc/open-axiom/trunk/src/algebra/boolean.spad.pamphlet?revision=2022&view=markup

-- Gaby

------------------------------------------------------------------------------
EditLive Enterprise is the world's most technically advanced content
authoring tool. Experience the power of Track Changes, Inline Image
Editing and ensure content is compliant with Accessibility Checking.
http://p.sf.net/sfu/ephox-dev2dev

Re: [open-axiom-devel] Re: computation framework

On Monday 20 Jun 2011 18:57:22 Gabriel Dos Reis wrote:
> If you want to support intuitionistic logic, you cannot simplify
> double negation.  See my comment in the definition of simplifyOneStep
> in the package PropositionalFormulaFunctions1

Gaby,

So is boolean.spad.pamphlet general enough to support intuitionistic logic?

Martin

------------------------------------------------------------------------------
EditLive Enterprise is the world's most technically advanced content
authoring tool. Experience the power of Track Changes, Inline Image
Editing and ensure content is compliant with Accessibility Checking.
http://p.sf.net/sfu/ephox-dev2dev

Re: [open-axiom-devel] computation framework

Martin Baker <ax87438@...> writes:

| On Monday 20 Jun 2011 18:57:22 Gabriel Dos Reis wrote:
| > If you want to support intuitionistic logic, you cannot simplify
| > double negation.  See my comment in the definition of simplifyOneStep
| > in the package PropositionalFormulaFunctions1
| 
| Gaby,
| 
| So is boolean.spad.pamphlet general enough to support intuitionistic logic?

OpenAxiom, and I believe all flavours of AXIOM, makes implicit use of
classical logic.  So, to avoid surprises, I assumed classical logic in
the simplifier.  However, for that particular algebra, that is easily
fixed by removing the line

   (f1' := isNot f1) case F => f1' -- assume classical logic 

from simplifyOneStep.  If that is done then boolean.spad.pamphlet
is general enough to support intuitionistic logic.
I believe the rules that `dual' uses are OK.

A long time ago, for the purposes of semantics-based program analysis, I
introduced the domain KleeneTrivalentLogic (also in
boolean.spad.pamphlet) which I views as a fairly good compromise
(from computational perspective).  Because of some misguided parser
simplifications (all flavours of AXIOM affected, OpenAxiom much less),
you have to be careful about how you write logical formulae with values
from the domain KleeneTrivalentLogic.

[open-axiom-devel] Check for HyperDoc and others at runtime

------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev

_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@...
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel

Re: [open-axiom-devel] Check for HyperDoc and others at runtime

Igor Pashev wrote:
> 
> Hi, All!
> 
> I'm trying to package Open Axiom for Debian
> keeping Debian scheme to have separated
> packages for separated programmes:
> http://packages.debian.org/source/sid/axiom
> 
> The problem is that Open Axiom package
> can be installed without graphics or HyperDoc,
> but OpenAxiom will try ro run them, infinitly
> respawning its forks (they die because
> there is no such file).
> 
> So I propose a wayt to detect presence of
> additional programmes and do not start them,
> if they are absent.
> 

It seems that you are packaging Axiom which is a different
project with different mailing list (axiom-developer@...).

--

-- 
                              Waldek Hebisch
hebisch@... 

------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev

Re: [open-axiom-devel] Check for HyperDoc and others at runtime

------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev

_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@...
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel

Re: [open-axiom-devel] Check for HyperDoc and others at runtime

Игорь Пашев <pashev.igor <at> gmail.com> writes:

| Hi, All!
| 
| I'm trying to package Open Axiom for Debian
| keeping Debian scheme to have separated
| packages for separated programmes:
| http://packages.debian.org/source/sid/axiom
| 
| The problem is that Open Axiom package
| can be installed without graphics or HyperDoc,
| but OpenAxiom will try ro run them, infinitly
| respawning its forks (they die because
| there is no such file).

Hi Igor,

glad to hear from you.  I believe there was a bug in OpenAxiom-1.4.0
in that it did not build viewman but would try to spawn it.  That had
been fixed since then and the fix is part of the next OpenAxiom-1.4.1
release (hopefully, before the Sunday.)

| So I propose a wayt to detect presence of
| additional programmes and do not start them,
| if they are absent.

I agreed.  Usually, we detect at configure time whether the host has
X11.  Then at use time, we refuse to start the graphics component if
user requests it.  There was a glitch when I added a new GUI interface
for Windows platforms.

Could you test the 1.4.x branch and tell me whether you still see the
problem?  Thanks!

-- Gaby

------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel

Re: [open-axiom-devel] Check for HyperDoc and others at runtime

------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev

_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@...
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel