Journal of Formalized Mathematics, Volume 15, 2003

Table of contents

1. Improvement of Radix-$2^k$ Signed-Digit Number for High Speed Circuit
   by Masaaki Niimura and Yasushi Fuwa
   
2. High Speed Adder Algorithm with Radix-$2^k$ SD\_Sub Number
   by Masaaki Niimura and Yasushi Fuwa
   
3. The Underlying Principle of Dijkstra's Shortest Path Algorithm
   by Jing-Chao Chen and Yatsuka Nakamura
   
4. On the Hausdorff Distance Between Compact Subsets
   by Adam Grabowski
   
5. Chains on a Grating in Euclidean Space
   by Freek Wiedijk
   
6. Bessel's Inequality
   by Hiroshi Yamazaki, Yasunari Shidama, and Yatsuka Nakamura
   
7. A Representation of Integers by Binary Arithmetics and Addition of Integers
   by Hisayoshi Kunimune and Yatsuka Nakamura
   
8. The Inner Product of Finite Sequences and of Points of $n$-dimensional Topological Space
   by Kanchun and Yatsuka Nakamura
   
9. Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients
   by Xiquan Liang
   
10. Morphism Into Chains, Part I
    by Artur Kornilowicz
    
11. Propositional Calculus for Boolean Valued Functions, VII
    by Shunichi Kobayashi
    
12. Basic Notions and Properties of Orthoposets
    by Markus Moschner
    
13. Dijkstra's Shortest Path Algorithm
    by Jing-Chao Chen
    
14. General Fashoda Meet Theorem for Unit Circle and Square
    by Yatsuka Nakamura
    
15. On Some Properties of Real Hilbert Space, I
    by Hiroshi Yamazaki, Yasumasa Suzuki, Takao Inoue, and Yasunari Shidama
    
16. Full Subtracter Circuit. Part II
    by Shin'nosuke Yamaguchi, Grzegorz Bancerek, and Katsumi Wasaki
    
17. Real Linear Space of Real Sequences
    by Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama
    
18. Hilbert Space of Real Sequences
    by Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama
    
19. Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator, Part I
    by Takao Inoue
    
20. Some Properties for Convex Combinations
    by Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama
    
21. On Some Properties of Real Hilbert Space, II
    by Hiroshi Yamazaki, Yasumasa Suzuki, Takao Inoue, and Yasunari Shidama
    
22. Inner Products and Angles of Complex Numbers
    by Wenpai Chang and Yatsuka Nakamura
    
23. Angle and Triangle in Euclidian Topological Space
    by Akihiro Kubo and Yatsuka Nakamura
    
24. The Class of Series-Parallel Graphs, II
    by Krzysztof Retel
    
25. Characterization and Existence of Gr\"obner Bases
    by Christoph Schwarzweller
    
26. Construction of Gr\"obner bases. S-Polynomials and Standard Representations
    by Christoph Schwarzweller
    
27. On the Subcontinua of a Real Line
    by Adam Grabowski
    
28. On the Kuratowski Closure-Complement Problem
    by Lilla Krystyna Baginska and Adam Grabowski
    
29. Convex Hull, Set of Convex Combinations and Convex Cone
    by Noboru Endou and Yasunari Shidama
    
30. On the Two Short Axiomatizations of Ortholattices
    by Wioletta Truszkowska and Adam Grabowski
    
31. Definition of Convex Function and Jensen's Inequality
    by Grigory E. Ivanov
    
32. On Semilattice Structure of Mizar Types
    by Grzegorz Bancerek
    
33. Lines in $n$-Dimensional Euclidean Spaces
    by Akihiro Kubo
    
34. Banach Space of Absolute Summable Real Sequences
    by Yasumasa Suzuki, Noboru Endou, and Yasunari Shidama
    
35. Cross Products and Tripple Vector Products in 3-dimensional Euclidian Space
    by Kanchun , Hiroshi Yamazaki, and Yatsuka Nakamura
    
36. Calculation of Matrices of Field Elements. Part I
    by Yatsuka Nakamura and Hiroshi Yamazaki
    
37. Lattice of Fuzzy Sets
    by Takashi Mitsuishi and Grzegorz Bancerek
    
38. On the Kuratowski Limit Operators
    by Adam Grabowski
    
39. On the Segmentation of a Simple Closed Curve
    by Andrzej Trybulec
    
40. On the Sets Inhabited by Numbers
    by Andrzej Trybulec
    
41. On the Calculus of Binary Arithmetics
    by Shunichi Kobayashi
    
42. SCMPDS Is Not Standard
    by Artur Kornilowicz and Yasunari Shidama
    
43. On the Upper and Lower Approximations of the Curve
    by Robert Milewski
    
44. Sorting Operators for Finite Sequences
    by Yatsuka Nakamura
    
45. Magnitude Relation Properties of Radix-$2^k$ SD Number
    by Masaaki Niimura and Yasushi Fuwa
    
46. High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number
    by Masaaki Niimura and Yasushi Fuwa
    
47. Transitive Closure of Fuzzy Relations
    by Takashi Mitsuishi and Grzegorz Bancerek
    
48. Basic Properties of Rough Sets and Rough Membership Function
    by Adam Grabowski
    
49. Correctness of Non Overwriting Programs. Part I
    by Yatsuka Nakamura
    
50. A Tree of Execution of a Macroinstruction
    by Artur Kornilowicz
    
51. Banach Space of Bounded Linear Operators
    by Yasunari Shidama
    
52. Little Bezout Theorem (Factor Theorem)
    by Piotr Rudnicki
    
53. Primitive Roots of Unity and Cyclotomic Polynomials
    by Broderic Arneson and Piotr Rudnicki
    
54. Witt's Proof of the Wedderburn Theorem
    by Broderic Arneson, Matthias Baaz, and Piotr Rudnicki