Search results for "Mizar"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
239	Grzegorz Bancerek, Josef Urban	Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles.	MKM	2004	DBLP DOI BibTeX RDF
226	Josef Urban	MPTP 0.2: Design, Implementation, and Initial Experiments.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	MPTP, Mizar, ATP, MPA, re-proving, proof discovery, MML
164	Josef Urban, Geoff Sutcliffe	ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments.	Math. Comput. Sci.	2008	DBLP DOI BibTeX RDF	verification, automated reasoning, Formalized mathematics
164	Josef Urban	XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy.	MKM	2005	DBLP DOI BibTeX RDF
146	Freek Wiedijk	Mizar's Soft Type System.	TPHOLs	2007	DBLP DOI BibTeX RDF
146	Ewa Borak, Anna Zalewska	Mizar Course in Logic and Set Theory.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
128	Josef Urban, Geoff Sutcliffe	ATP Cross-Verification of the Mizar MPTP Challenge Problems.	LPAR	2007	DBLP DOI BibTeX RDF
120	Josef Urban	MPTP - Motivation, Implementation, First Experiments.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	ATP, Mizar, MPA, MPTP
106	Paul A. Cairns, Jeremy Gow	Integrating Searching and Authoring in Mizar.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Alcor, Mizar, Information retrieval, Mathematics, LSI
93	Adam Naumowicz, Czeslaw Bylinski	Improving Mizar Texts with Properties and Requirements.	MKM	2004	DBLP DOI BibTeX RDF
75	Gilbert Lee, Piotr Rudnicki	Alternative Aggregates in Mizar.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
75	Freek Wiedijk	Mizar Light for HOL Light.	TPHOLs	2001	DBLP DOI BibTeX RDF
75	Christoph Schwarzweller	Mizar Correctness Proofs of Generic Fraction Field Arithmetic.	Generic Programming	1998	DBLP DOI BibTeX RDF
71	Grzegorz Bancerek	Information Retrieval and Rendering with.	MKM	2006	DBLP DOI BibTeX RDF
57	Adam Naumowicz, Artur Kornilowicz	A Brief Overview of Mizar.	TPHOLs	2009	DBLP DOI BibTeX RDF
57	Christoph Schwarzweller	Gröbner Bases - Theory Refinement in the Mizar System.	MKM	2005	DBLP DOI BibTeX RDF
57	Paul A. Cairns	Informalising Formal Mathematics: Searching the Mizar Library with Latent Semantics.	MKM	2004	DBLP DOI BibTeX RDF
57	Josef Urban	Translating Mizar for First Order Theorem Provers.	MKM	2003	DBLP DOI BibTeX RDF
53	Fairouz Kamareddine	The Gradual Computerisation of Mathematics in MathLang.	SYNASC	2007	DBLP DOI BibTeX RDF
43	Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz 0001, Martin Suda 0001, Josef Urban	MizAR 60 for Mizar 50.	CoRR	2023	DBLP DOI BibTeX RDF
43	Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz 0001, Martin Suda 0001, Josef Urban	MizAR 60 for Mizar 50.	ITP	2023	DBLP DOI BibTeX RDF
43	Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak	The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar.	J. Autom. Reason.	2018	DBLP DOI BibTeX RDF
43	Adam Naumowicz, Radoslaw Piliszek	Accessing the Mizar Library with a Weakly Strict Mizar Parser.	CICM	2016	DBLP DOI BibTeX RDF
43	Cezary Kaliszyk, Josef Urban	MizAR 40 for Mizar 40.	J. Autom. Reason.	2015	DBLP DOI BibTeX RDF
43	Cezary Kaliszyk, Josef Urban	MizAR 40 for Mizar 40.	CoRR	2013	DBLP BibTeX RDF
43	Jesse Alama	mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library	CoRR	2011	DBLP BibTeX RDF
43	Jesse Alama	mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
39	Adam Grabowski, Christoph Schwarzweller	Rough Concept Analysis - Theory Development in the Mizar System.	MKM	2004	DBLP DOI BibTeX RDF
39	Parveen Gartan, Fahimeh Khorsand, Pushpak Mizar, Juha Ilmari Vahokovski, Luis F. Cervantes, Bengt Erik Haug, Ruth Brenk, Charles L. Brooks III, Nathalie Reuter	Investigating Polypharmacology through Targeting Known Human Neutrophil Elastase Inhibitors to Proteinase 3.	J. Chem. Inf. Model.	2024	DBLP DOI BibTeX RDF
39	Mizar Luca Federici, Lorenza Manenti, Sara Manzoni	A Checklist for the Evaluation of Pedestrian Simulation Software Functionalities.	CoRR	2014	DBLP BibTeX RDF
39	Mizar Luca Federici, Andrea Gorrini, Lorenza Manenti, Fabio Sartori	Festivalization of the City Support: A Case Study.	MTSR	2012	DBLP DOI BibTeX RDF
39	Mizar Luca Federici, Andrea Gorrini, Lorenza Manenti, Fabio Sartori	A Proposal of an Event Ontology for Urban Crowd Profiling.	CAiSE Workshops	2012	DBLP DOI BibTeX RDF
39	Mizar Luca Federici, Andrea Gorrini, Lorenza Manenti, Giuseppe Vizzari	Data Collection for Modeling and Simulation: Case Study at the University of Milan-Bicocca.	ACRI	2012	DBLP DOI BibTeX RDF
39	Stefania Bandini, Mizar Luca Federici, Giuseppe Vizzari	Situated Cellular Agents Approach to Crowd Modeling and Simulation.	Cybern. Syst.	2007	DBLP DOI BibTeX RDF
39	Stefania Bandini, Mizar Luca Federici, Sara Manzoni	SCA approach to micro-scale modelling of paradigmatic emergent crowd behaviors.	SCSC	2007	DBLP BibTeX RDF
39	Stefania Bandini, Mizar Luca Federici, Sara Manzoni	A qualitative evaluation of technologies and techniques for data collection on pedestrians and crowded situations.	SCSC	2007	DBLP BibTeX RDF	data collection, crowds
39	Stefania Bandini, Mizar Luca Federici, Sara Manzoni, Giuseppe Vizzari	Pedestrian and Crowd Dynamics Simulation: Testing SCA on Paradigmatic Cases of Emerging Coordination in Negative Interaction Conditions.	PaCT	2007	DBLP DOI BibTeX RDF	Paradigmatic Cases, Lane Formation, Freezing by Heating, Situated Cellular Agents, Multi-Agent System, Crowd Simulation
39	Mizar Luca Federici, Stefano Redaelli, Giuseppe Vizzari	Models, Abstractions and Phases in Multi-Agent Based Simulation.	WOA	2006	DBLP BibTeX RDF
39	Giuseppe Vizzari, Giorgio Pizzi, Mizar Luca Federici	Visualization of Discrete Crowd Dynamics in a 3D Environment.	ACRI	2006	DBLP DOI BibTeX RDF
39	Stefania Bandini, Mizar Luca Federici, Giuseppe Vizzari	A Methodology for Crowd Modelling with Situated Cellular Agents.	WOA	2005	DBLP BibTeX RDF
39	Stefania Bandini, Mizar Luca Federici, Sara Manzoni, Giuseppe Vizzari	Towards a Methodology for Situated Cellular Agent Based Crowd Simulations.	ESAW	2005	DBLP DOI BibTeX RDF
36	Agnieszka Rowinska-Schwarzweller, Christoph Schwarzweller	Towards Mathematical Knowledge Management for Electrical Engineering.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
36	Adam Grabowski, Markus Moschner	Managing Heterogeneous Theories within a Mathematical Knowledge Repository.	MKM	2004	DBLP DOI BibTeX RDF
36	Grzegorz Bancerek, Piotr Rudnicki	Information Retrieval in MML.	MKM	2003	DBLP DOI BibTeX RDF
36	Vincent Zammit	On the Implementation of an Extensible Declarative Proof Language.	TPHOLs	1999	DBLP DOI BibTeX RDF
22	Mario Carneiro	Reimplementing Mizar in Rust.	CoRR	2023	DBLP DOI BibTeX RDF
22	Christoph Schwarzweller	Developing Field Theory in Mizar.	FedCSIS	2023	DBLP DOI BibTeX RDF
22	Adam Grabowski, Artur Kornilowicz	Implementing More Explicit Definitional Expansions in Mizar (Short Paper).	ITP	2023	DBLP DOI BibTeX RDF
22	Mario Carneiro	Reimplementing Mizar in Rust.	ITP	2023	DBLP DOI BibTeX RDF
22	Adam Naumowicz	Extending Numeric Automation for Number Theory Formalizations in Mizar.	CICM	2023	DBLP DOI BibTeX RDF
22	Hideharu Furushima, Daichi Yamamichi, Seigo Shigenaka, Kazuhisa Nakasho, Katsumi Wasaki	An Integrated Web Platform for the Mizar Mathematical Library.	CoRR	2022	DBLP DOI BibTeX RDF
22	Hideharu Furushima, Daichi Yamamichi, Seigo Shigenaka, Kazuhisa Nakasho, Katsumi Wasaki	An Integrated Web Platform for the Mizar Mathematical Library.	CICM	2022	DBLP DOI BibTeX RDF
22	Adam Grabowski	Fuzzy Implications in the Mizar System.	FUZZ-IEEE	2021	DBLP DOI BibTeX RDF
22	Hirota Taniguchi, Kazuhisa Nakasho	Visual Studio Code Extension and Auto-completion for Mizar Language.	CANDAR	2021	DBLP DOI BibTeX RDF
22	Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz	Syntactic-Semantic Form of Mizar Articles.	ITP	2021	DBLP DOI BibTeX RDF
22	Colin Rothgang, Artur Kornilowicz, Florian Rabe 0001	A New Export of the Mizar Mathematical Library.	CICM	2021	DBLP DOI BibTeX RDF
22	Daichi Yamamichi, Seigo Shigenaka, Kazuhisa Nakasho, Katsumi Wasaki	A Web Platform for Hosting the Mizar Mathematical Library (short paper).	CICM Workshops	2021	DBLP BibTeX RDF
22	Karol Pak	Formalization of Prime Representing Polynomial in Mizar (short paper).	CICM Workshops	2021	DBLP BibTeX RDF
22	Sebastian Koch	Unification of Graphs and Relations in Mizar.	Formaliz. Math.	2020	DBLP DOI BibTeX RDF
22	Artur Kornilowicz	Enhancement of properties in Mizar.	PeerJ Comput. Sci.	2020	DBLP DOI BibTeX RDF
22	Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban	Exploration of neural machine translation in autoformalization of mathematics in Mizar.	CPP	2020	DBLP DOI BibTeX RDF
22	Adam Naumowicz	An Experiment on Mizar Adjectives with Extra Visible Arguments.	SYNASC	2020	DBLP DOI BibTeX RDF
22	Adam Naumowicz	Dataset Description: Formalization of Elementary Number Theory in Mizar.	CICM	2020	DBLP DOI BibTeX RDF
22	Karol Pak	Formalization of the MRDP Theorem in the Mizar System.	Formaliz. Math.	2019	DBLP DOI BibTeX RDF
22	Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban	Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar.	CoRR	2019	DBLP BibTeX RDF
22	Jan Jakubuv, Josef Urban	Hammering Mizar by Learning Clause Guidance.	CoRR	2019	DBLP BibTeX RDF
22	Cezary Kaliszyk, Karol Pak	Semantics of Mizar as an Isabelle Object Logic.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
22	Kazuhisa Nakasho	Development of a Flexible Mizar Tokenizer and Parser for Information Retrieval System.	FedCSIS	2019	DBLP DOI BibTeX RDF
22	Jan Jakubuv, Josef Urban	Hammering Mizar by Learning Clause Guidance (Short Paper).	ITP	2019	DBLP DOI BibTeX RDF
22	Artur Kornilowicz	Sethood Property in Mizar.	CICM Workshops	2019	DBLP BibTeX RDF
22	Adam Naumowicz	Testing Mizar User Interactivity in a University-level Introductory Course on Foundations of Mathematics.	CICM Workshops	2019	DBLP BibTeX RDF
22	Adrian Jaszczak	Formal verification of the correctness of chosen algorithms in Mizar.	CICM Workshops	2019	DBLP BibTeX RDF
22	Adam Grabowski	Constructing Examples of Fuzzy Implications within the Mizar Mathematical Library.	CICM Workshops	2019	DBLP BibTeX RDF
22	Ievgen Ivanov, Artur Kornilowicz, Mykola S. Nikitchenko	Implementation of the Composition-nominative Approach to Program Formalization in Mizar.	Comput. Sci. J. Moldova	2018	DBLP BibTeX RDF
22	Karol Pak	Combining the Syntactic and Semantic Representations of Mizar Proofs.	FedCSIS	2018	DBLP DOI BibTeX RDF
22	Karol Pak	Mizar Set Comprehension in Isabelle Framework.	FedCSIS (Communication Papers)	2018	DBLP DOI BibTeX RDF
22	Cezary Kaliszyk, Karol Pak	Isabelle Import Infrastructure for the Mizar Mathematical Library.	CICM	2018	DBLP DOI BibTeX RDF
22	Grzegorz Bancerek, Adam Naumowicz, Josef Urban	System Description: XSL-Based Translator of Mizar to LaTeX.	CICM	2018	DBLP DOI BibTeX RDF
22	Karol Pak	Progress in the Formalization of Matiyasevich's Theorem in the Mizar System.	CICM Workshops	2018	DBLP BibTeX RDF
22	Adam Naumowicz, Artur Kornilowicz	Introducing Euclidean Relations to Mizar.	FedCSIS	2017	DBLP DOI BibTeX RDF
22	Artur Kornilowicz, Andrii Kryvolap, Mykola S. Nikitchenko, Ievgen Ivanov	Formalization of the Algebra of Nominative Data in Mizar.	FedCSIS	2017	DBLP DOI BibTeX RDF
22	Marcin Acewicz, Karol Pak	Formalization of Pell's Equations in the Mizar System.	FedCSIS	2017	DBLP DOI BibTeX RDF
22	Cezary Kaliszyk, Karol Pak	Progress in the Independent Certification of Mizar Mathematical Library in Isabelle.	FedCSIS	2017	DBLP DOI BibTeX RDF
22	Cezary Kaliszyk, Josef Urban, Jirí Vyskocil	System Description: Statistical Parsing of Informalized Mizar Formulas.	SYNASC	2017	DBLP DOI BibTeX RDF
22	Adam Grabowski	Expressing the Notion of a Mathematical Structure in the Formal Language of Mizar.	ICMMI	2017	DBLP DOI BibTeX RDF
22	Cezary Kaliszyk, Karol Pak	Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic.	CICM	2017	DBLP DOI BibTeX RDF
22	Adam Naumowicz	Towards Standardized Mizar Environments.	ISAT (2)	2017	DBLP DOI BibTeX RDF
22	Artur Kornilowicz, Andrii Kryvolap, Mykola S. Nikitchenko, Ievgen Ivanov	Formalization of the Nominative Algorithmic Algebra in Mizar.	ISAT (2)	2017	DBLP DOI BibTeX RDF
22	Adam Grabowski	Lattice Theory for Rough Sets - A Case Study with Mizar.	Fundam. Informaticae	2016	DBLP DOI BibTeX RDF
22	Chad E. Brown, Josef Urban	Extracting Higher-Order Goals from the Mizar Mathematical Library.	CoRR	2016	DBLP BibTeX RDF
22	Hiroyuki Okazaki, Yuichi Futa	Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar.	FM4M/MathUI/ThEdu/DP/WIP@CIKM	2016	DBLP BibTeX RDF
22	Adam Naumowicz	Linking to Compound Conditions in Mizar.	FM4M/MathUI/ThEdu/DP/WIP@CIKM	2016	DBLP BibTeX RDF
22	Artur Kornilowicz	Registrations vs Redefinitions in Mizar.	FM4M/MathUI/ThEdu/DP/WIP@CIKM	2016	DBLP BibTeX RDF
22	Adam Grabowski, Roland Coghetto	Tarski's Geometry and the Euclidean Plane in Mizar.	FM4M/MathUI/ThEdu/DP/WIP@CIKM	2016	DBLP BibTeX RDF
22	Adam Grabowski	Tarski's geometry modelled in Mizar computerized proof assistant.	FedCSIS	2016	DBLP DOI BibTeX RDF
22	Adam Grabowski, Artur Kornilowicz, Christoph Schwarzweller	On algebraic hierarchies in mathematical repository of Mizar.	FedCSIS	2016	DBLP DOI BibTeX RDF
22	Cezary Kaliszyk, Karol Pak, Josef Urban	Towards a mizar environment for isabelle: foundations and language.	CPP	2016	DBLP DOI BibTeX RDF
22	Hiroyuki Okazaki	Formalization of statistical indistinguishability of probability distribution ensembles in Mizar.	ISITA	2016	DBLP BibTeX RDF
22	Artur Kornilowicz	Enhancement of Mizar Texts with Transitivity Property of Predicates.	CICM	2016	DBLP DOI BibTeX RDF
22	Chad E. Brown, Josef Urban	Extracting Higher-Order Goals from the Mizar Mathematical Library.	CICM	2016	DBLP DOI BibTeX RDF