| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
| H A D | bound_propagator.cpp | 294 bk = AXIOM; // don't need justification at level 0 in assert_lower_core()
346 bk = AXIOM; // don't need justification at level 0 in assert_upper_core()
794 if (b->m_kind == AXIOM || b->m_kind == DECISION) in explain()
|
| /dports/math/fricas/fricas-1.3.7/src/ |
| H A D | Makenotes.tex | 315 \bibitem{2} \$AXIOM/src/etc/asq.c.pamphlet
316 \bibitem{3} \$AXIOM/src/clef/edible.c.pamphlet
|
| /dports/math/vampire/vampire-4.5.1/Kernel/ |
| H A D | Inference.cpp | 350 …initDefault(UnitInputType::AXIOM /* the minimal element; we later compute maximum over premises*/,… in initMany()
390 init0(UnitInputType::AXIOM,ta.rule); in Inference()
|
| H A D | Inference.hpp | 46 AXIOM = 0, enumerator
|
| H A D | Clause.cpp | 90 inference().setInputType(UnitInputType::AXIOM); in Clause()
|
| /dports/math/vampire/vampire-4.5.1/VUtils/ |
| H A D | Z3InterpolantExtractor.cpp | 379 FormulaUnit* lemmaUnit = new FormulaUnit(lemma, inf, Unit::AXIOM); in readProofObject()
447 FormulaUnit* resUnit = new FormulaUnit(conclusion, inf, Unit::AXIOM); in readProofObject()
|
| H A D | LocalityRestoring.cpp | 292 FormulaUnit* res = new FormulaUnit(form, new Inference0(Inference::INPUT), Unit::AXIOM); in makeNSCPremise()
680 FormulaUnit* res = new FormulaUnit(form, inf, Unit::AXIOM); in getFringeUnit()
|
| /dports/math/maxima/maxima-5.43.2/tests/ |
| H A D | rtestode_zp.mac | 3 AXIOM, DERIVE, MACSYMA, MATHEMATICA, MUPAD and REDUCE
|
| /dports/math/fricas/fricas-1.3.7/src/algebra/ |
| H A D | fff.spad | 11 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
12 ++ AXIOM Technical Report Series, ATR/5 NP2522.
|
| H A D | ffhom.spad | 12 ++ J. Grabmeier, A. Scheerhorn: Finite Fields in AXIOM.
13 ++ AXIOM Technical Report Series, ATR/5 NP2522.
|
| /dports/math/vampire/vampire-4.5.1/Shell/ |
| H A D | InterpolantMinimizer.cpp | 528 …getArrayishObjectIterator(lits, len),NonspecificInference0(UnitInputType::AXIOM,InferenceRule::INP… in getComponent()
567 NonspecificInference0(UnitInputType::AXIOM,InferenceRule::INPUT)); in getAtomComponent()
|
| H A D | EqualityProxy.cpp | 375 …FormulaUnit* defUnit = new FormulaUnit(quantDefForm,NonspecificInference0(UnitInputType::AXIOM,Inf… in getProxyPredicate()
|
| H A D | AnswerExtractor.cpp | 483 …res = Clause::fromIterator(getSingletonIterator(lit),NonspecificInference0(UnitInputType::AXIOM,In… in getResolverClause()
|
| H A D | Skolem.cpp | 456 …Unit* defUnit = new FormulaUnit(def,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::CHOI… in skolemise()
|
| H A D | TPTPPrinter.cpp | 179 case UnitInputType::AXIOM: in printTffWrapper()
|
| /dports/math/fricas/fricas-1.3.7/pre-generated/target/share/spadhelp/ |
| H A D | String.help | 215 o $AXIOM/doc/src/algebra/string.spad.dvi
|
| /dports/math/vampire/vampire-4.5.1/Api/ |
| H A D | FormulaBuilder.hpp | 151 AXIOM, enumerator
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_context_pp.cpp | 617 case b_justification::AXIOM: in display()
646 case b_justification::AXIOM: in display_compact_j()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_context_pp.cpp | 591 case b_justification::AXIOM: in display()
620 case b_justification::AXIOM: in display_compact_j()
|
| /dports/math/fricas/fricas-1.3.7/src/doc/ht/ |
| H A D | expose.ht | 46 \item\tab{3}{\em naglink}\tab{13}All constructors used in the AXIOM NAG Link
|
| /dports/math/fricas/fricas-1.3.7/pre-generated/target/share/hypertex/pages/ |
| H A D | expose.ht | 46 \item\tab{3}{\em naglink}\tab{13}All constructors used in the AXIOM NAG Link
|
| /dports/math/vampire/vampire-4.5.1/Saturation/ |
| H A D | SaturationAlgorithm.cpp | 636 sosForAxioms = sosForAxioms && cl->inputType()==UnitInputType::AXIOM; in addInputClause()
688 ASS_EQ(toNumber(cl->inputType()),toNumber(UnitInputType::AXIOM)); in addInputSOSClause()
|
| /dports/math/fricas/fricas-1.3.7/ |
| H A D | CHANGELOG.old | 135 20051030 tpd src/etc/Makefile remove AXIOM variable from axiom cmd
260 20050518 tpd zips/noweb.src.Makefile.patch make noweb respect $AXIOM
511 20050112 wsp src/interp/debugsys.lisp use $AXIOM rather than hardcoded paths
648 20041221 swx src/interp/debugsys.boot build debugsys w.r.t $AXIOM
689 20041028 tpd src/etc/axiom change clef to $AXIOM/bin/clef
931 20031031 tpd src/lib/sockio-c.c kill AXIOM socket message
937 20031030 tpd src/etc/Makefile build axiom command in $AXIOM/bin
|
| /dports/math/vampire/vampire-4.5.1/Parse/ |
| H A D | SMTLIB.cpp | 1329 FormulaUnit* fu = new FormulaUnit(f, new Inference0(Inference::INPUT), Unit::AXIOM); in buildFormula()
1443 FormulaUnit* def = new FormulaUnit(df, new Inference0(Inference::INPUT), Unit::AXIOM); in nameFormula()
|
| /dports/math/vampire/vampire-4.5.1/FMB/ |
| H A D | FiniteModelBuilder.cpp | 1756 …Clause* empty = new(0) Clause(0,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::MODEL_NO… in runImpl()
1795 …Clause* empty = new(0) Clause(0,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::MODEL_NO… in runImpl()
2237 …new FormulaUnit(predDefGround, NonspecificInference0(UnitInputType::AXIOM, InferenceRule::INPUT))); in onModelFound()
|