@INCOLLECTION{farmer-at65,
AUTHOR = {Farmer, William},
TITLE = {Chiron: A Multi-Paradigm Logic},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {1--19},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{omyla-at65,
AUTHOR = {Omy{\l}a, Mieczys{\l}aw},
TITLE = {Remarks on Non-{F}regean Logic},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {21--31},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{liang-at65,
AUTHOR = {Liang, Xiquan and Ge, Fuguo and Yan, Li},
TITLE = {Some Logical Aspects of Mathematical Reasoning},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {33--44},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{hales-at65,
AUTHOR = {Hales, Thomas},
TITLE = {Jordan's Proof of the {J}ordan Curve Theorem},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {45--60},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{tryb-swie-at65,
AUTHOR = {Trybulec, Zinaida and Swieczkowska, Halina},
TITLE = {Some Remarks on The Language of Mathematical Texts},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {61--73},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{kerb-poll-at65,
AUTHOR = {Kerber, Manfred and Pollet, Martin},
TITLE = {Informal and Formal Representations in Mathematics},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {75--94},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{kama-maar-rete-well-at65,
AUTHOR = {Kamareddine, Fairouz and Maarek, Manuel and Retel, Krzysztof and Weels, J.B.},
TITLE = {Gradual Computerisation/Formalisation of Mathematical Texts into {M}izar},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {95--120},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{wiedijk-at65,
AUTHOR = {Wiedijk, Freek},
TITLE = {The {QED} Manifesto Revisited},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {121--133},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{mcca-bund-aute-at65,
AUTHOR = {McCasland, Roy and Bundy, Alan and Autexier, Serge},
TITLE = {Automated Discovery of Inductive Theorems},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {135--149},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{harrison-at65,
AUTHOR = {Harrison, John},
TITLE = {Formalizing Basic Complex Analysis},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {151--165},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{shid-endo-kawa-at65,
AUTHOR = {Shidama, Yasunari and Endou, Noburu and Kawamoto, Pauline},
TITLE = {On the Formalization of {L}ebesgue Integrals},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {167--177},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{grab-korn-at65,
AUTHOR = {Grabowski, Adam and Korni{\l}owicz, Artur},
TITLE = {Computer-Assisted Reasoning about Algebraic Topology},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {179--189},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{naumowicz-at65,
AUTHOR = {Naumowicz, Adam},
TITLE = {Evaluating Prospective Built-in Elements of Computer Algebra in {M}izar},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {191--200},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{nakamura-at65,
AUTHOR = {Nakamura, Yatsuka},
TITLE = {Proving the Correctness of Functional Programs using {M}izar},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {201--211},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{wasaki-at65,
AUTHOR = {Wasaki, Katsumi},
TITLE = {A Verification for Redundant Signed Digit Adder Cicuits},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {213--230},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{siek-aute-at65,
AUTHOR = {Siekmann, J{\"o}rg and Autexier, Serge},
TITLE = {Computer Supported Formal Work: Towards a Digital Mathematical Assistant},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {231--248},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{gow-cair-at65,
AUTHOR = {Gow, Jeremy and Cairns, Paul},
TITLE = {Closing the Gap Between Formal and Digital Libraries of Mathematics},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {249--263},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{banc-kohl-at65,
AUTHOR = {Bancerek, Grzegorz and Kohlhase, Michael},
TITLE = {Towards a {M}izar {M}athematical {L}ibrary in {OMD}oc Format},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {265--275},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{wenzel-at65,
AUTHOR = {Wenzel, Makarius},
TITLE = {Isabelle/{I}sar - a Generic Framework for Human-Readable Proof Documents},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {277--297},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{benz-brow-at65,
AUTHOR = {Benzm{\"u}ller, Christoph and Brown, Chad},
TITLE = {The Curious Inference of {B}oolos in {M}izar and {OMEGA}},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {299--386},
URL={http://mizar.org/trybulec65/},
}
@INCOLLECTION{schwarzweller-at65,
AUTHOR = {Schwarzweller, Christoph},
TITLE = {Mizar Attributes: A Technique to Encode Mathematical Knowledge into Type Systems},
BOOKTITLE = {From Insight to Proof: Festschrift in Honour of Andrzej Trybulec},
SERIES = {Studies in Logic, Grammar and Rhetoric},
EDITOR = {Matuszewski, R. and Zalewska, A.},
PUBLISHER = {University of Bia{\l}ystok},
YEAR = {2007},
VOLUME = {10(23)},
PAGES = {387--400},
URL={http://mizar.org/trybulec65/},
}