I'm a computational mathematician (CM) so I'm coming to the logic area from left field (deep left, out by the fence). Thus my questionFor instance, in Axiom, Integers are: (1) -> )show Integer Integer is a domain constructor Abbreviation for Integer is INT This constructor is exposed in this frame. Issue )edit bookvol10.3.pamphlet to see algebra source code for INT ------------------------------- Operations -------------------------------- ?*? : (%,%) -> % ?*? : (Integer,%) -> % ?*? : (PositiveInteger,%) -> % ?**? : (%,PositiveInteger) -> % ?+? : (%,%) -> % ?-? : (%,%) -> % -? : % -> % ?<? : (%,%) -> Boolean ?<=? : (%,%) -> Boolean ?=? : (%,%) -> Boolean ?>? : (%,%) -> Boolean ?>=? : (%,%) -> Boolean D : % -> % D : (%,NonNegativeInteger) -> % OMwrite : (%,Boolean) -> String OMwrite : % -> String 1 : () -> % 0 : () -> % ?^? : (%,PositiveInteger) -> % abs : % -> % addmod : (%,%,%) -> % associates? : (%,%) -> Boolean base : () -> % binomial : (%,%) -> % bit? : (%,%) -> Boolean coerce : Integer -> % coerce : % -> % coerce : Integer -> % coerce : % -> OutputForm convert : % -> String convert : % -> DoubleFloat convert : % -> Float convert : % -> Pattern(Integer) convert : % -> InputForm convert : % -> Integer copy : % -> % dec : % -> % differentiate : % -> % even? : % -> Boolean factor : % -> Factored(%) factorial : % -> % gcd : List(%) -> % gcd : (%,%) -> % hash : % -> % hash : % -> SingleInteger inc : % -> % ..... etc. But that seems odd to me, in two ways. First, Proofs seem more like Once you give me the base ring I know what operations I can perform. Proofs seem to need the set of sequents and the set of hypotheses in order to be concrete, e.g. Proof(Heyting,LEM). Without specifying these constraints I have no idea what a "Proof" means computationally. You might also have to specify further information (ala Lakatos). At most, I might have a "refute" operation but nothing else leaps to mind. _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |