| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-06-26 | Working at the numbers.tex | Simon-Kor | |
| 2024-06-25 | Update equivalence.tex | adelon | |
| 2024-06-25 | [Stable] Implented continuous.tex and omitted some proves | Simon-Kor | |
| All changes till here are done such that the check of everything.tex will be a success. There are no logic flaws and false can't be proven with everything out of everthing.tex | |||
| 2024-06-25 | Improvement for the ATP proof time | Simon-Kor | |
| 2024-06-25 | Improvement for the ATP proof time | Simon-Kor | |
| 2024-06-25 | Sorted the structure of numbers.tex | Simon-Kor | |
| 2024-06-25 | definition of equivalence_from_partition can proof false in everything.tex | Simon-Kor | |
| 2024-06-20 | [Stable] Topologgical-space.tex | Simon-Kor | |
| 2024-06-20 | [Report] Task failed and was proven in the same time. | Simon-Kor | |
| The Line 182 has the goal to apply regular in a topological space. But if i try to prove it with Naproche ZF, then the task will be proven and the task fails in the same time. Console Output is the following: time stack exec zf -- --log library/topology/separation.tex -t 30 --dump ./dump [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fx,fB)&subseteq(fB,setminus(s__carrier(fX),fA))&subseteq(setminus(s__carrier(fX),fA),fU)). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,setminus(s__carrier(fX),setminus(s__carrier(fX),fU))=fU). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XN]:(elem(XN,neighbourhoods(fx,fX))&subseteq(XN,fU)&is_closed_in(XN,fX))). [Info] 00:00.21 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,(is_regular(fX)&is_kolmogorov(fX))<=>![XU]:(elem(XU,s__opens(fX))=>![Xx]:(elem(Xx,XU)=>?[XN]:(elem(XN,neighbourhoods(Xx,fX))&subseteq(XN,XU)&is_closed_in(XN,fX))))). [Info] 00:02.34 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))). [Info] 00:02.55 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(fB,setminus(s__carrier(fX),fA))). [Info] 00:08.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,closeds(fX))&elem(fx,fN)&subseteq(fN,fU)). [Info] 00:10.70 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(setminus(s__carrier(fX),fA),setminus(s__carrier(fX),setminus(s__carrier(fX),fU)))). [Info] 00:10.98 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,neighbourhoods(fx,fX))). Verification failed: prover found countermodel fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))).fof(is_regular,axiom,![XX]:(is_regular(XX)<=>![XV]:![Xp,XC]:((elem(Xp,s__carrier(XX))&~elem(Xp,XC)&elem(XC,closeds(XX)))=>?[XU,XC]:(elem(XU,s__opens(XX))&elem(XC,s__opens(XX))&elem(Xp,XU)&subseteq(XC,XV)&inter(XU,XV)=emptyset)))). fof(eqvilance_teethree_closed_neighbourhood_in_open1,axiom,elem(fx,s__carrier(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open2,axiom,~elem(fx,fC)). fof(eqvilance_teethree_closed_neighbourhood_in_open3,axiom,elem(fC,closeds(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open4,axiom,fC=setminus(s__carrier(fX),fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open5,axiom,elem(fx,fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open6,axiom,elem(fU,s__opens(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open7,axiom,is_regular(fX)&is_kolmogorov(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open8,axiom,inhabited(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open9,axiom,topological_space(fX)). real 0m14.914s user 0m37.867s sys 0m1.956s | |||
| 2024-06-18 | Merge remote-tracking branch 'upstream/main' | Simon-Kor | |
| 2024-06-18 | Definition of T3 and regular spaces. | Simon-Kor | |
| 2024-06-18 | Update topological-space.tex | adelon | |
| 2024-06-17 | Completed proofs [stable] | Simon-Kor | |
| 2024-06-16 | First implementation of basic relations of closed and open. | Simon-Kor | |
| Not finished. | |||
| 2024-06-12 | Prove Bug "Ex falso quodlibet" | Simon-Kor | |
| The generated ATP Tasks are done in few secounds, if they are send manually to Vampire. But if its done in Naproche all together it won't work. | |||
| 2024-06-11 | proof of complement_interior_eq_closure_complement and some more about ↵ | Simon-Kor | |
| clousures(unsatable) | |||
| 2024-06-04 | Proof of teetwo_space_is_teeone_space | Simon-Kor | |
| 2024-06-04 | Proof of teeone_implies_singletons_closed | Simon-Kor | |
| The Assumption was changed, for usage of bounded variables. Maybe there is a bug with Omitted. Omitted restricts the Ambigus Phrase testing. | |||
| 2024-06-04 | Some notation fixes and lemma for topo basis generats opens was proofed and ↵ | Simon-Kor | |
| optimizised | |||
| 2024-05-28 | Merge branch 'main' into main | Simon-Kor | |
| 2024-05-28 | unexpected behavior of vampire | Simon-Kor | |
| The task topological behavior is proofed in seconds by just vampire, but with mode casc it takes plenty seconds | |||
| 2024-05-28 | Update `inters_in_genopens` | adelon | |
| 2024-05-28 | Pow closed under binary intersection | adelon | |
| 2024-05-28 | Merge branch 'main' into main | Simon-Kor | |
| 2024-05-28 | proofing some lammes about topological basis | Simon-Kor | |
| 2024-05-25 | Prove `emptyset_open` to replace structure axiom | adelon | |
| 2024-05-23 | Update formatting | adelon | |
| 2024-05-22 | Update filter.tex | adelon | |
| 2024-05-22 | Add filter lemmas | adelon | |
| 2024-05-22 | Add lemma `filter_setminus_in` | adelon | |
| 2024-05-22 | Update label for `genopens` | adelon | |
| 2024-05-21 | Allow line breaks via `\textbox`, handle `\left`/`\right` | adelon | |
| 2024-05-21 | Add simple lemmas on filters | adelon | |
| 2024-05-16 | Fix missing `\text` | adelon | |
| 2024-05-14 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-05-14 | work on metric spaces | Simon-Kor | |
| 2024-05-14 | Update basis.tex | adelon | |
| 2024-05-07 | Merge branch 'adelon:main' into main | Simon-Kor | |
| 2024-05-07 | formalisation mertic optimized | Simon-Kor | |
| 2024-05-07 | Sketch noun coord, symbols for reals | adelon | |
| 2024-05-07 | Sketch lexicon mechanism | adelon | |
| 2024-05-07 | Clean up of Notation in numbers.tex | Simon-Kor | |
| First notation of tupels in the relation set was swapped with the canonical <. | |||
| 2024-05-07 | Formalization of metric spaces and some cleaning of numbers.tex | Simon-Kor | |
| Formalization of metric spaces: Therefore we introduced the predicate metric and its axiomatization. Then we introduced the term metric space in dependence of a metric function. This metric space is automatically a a topological space. | |||
| 2024-04-30 | Adding the first formalisation of reals | Simon-Kor | |
| 2024-04-13 | first formalisation of addition on naturals | Simon-Kor | |
| We try to Implement the Addition on natural numbers by a relation on N \times N to N such that some of the axioms of the addition holds | |||
| 2024-04-11 | Set the Headline Order for the corresponding section | Simon-Kor | |
| 2024-04-11 | Formalisation of groups and monoids | Simon-Kor | |
| The test.tex file was deleted and all formalisations of groups and monoids was moved to the fitting document of the library. Some proof steps of the new formalisation were optimized for proof time | |||
| 2024-03-31 | Possible_Bug | Simon-Kor | |
| In File test.tex line 51 could not be proven, error massage is in the new file error.txt | |||
| 2024-02-10 | Initial commit | adelon | |
 |
index : naproche-zf.git | |
| Unnamed repository; edit this file 'description' to name the repository. |
| summaryrefslogtreecommitdiff |