LTLFonts is a free font
containing mathematical symbols for typesetting formulas of linear
temporal logic (LTL) in the Manna/Pnueli notation. I designed it to be
used with the LaTeX typesetting system, but it should work with other
software as well.
The most recent version is 0.1.2. It is available to a small group of collaborators and should be consider a beta stage. The goal is to get feedback so I can improve the font.
There isn't much really, it's a circle and a square, but a few points to keep in mind are:
The font is distributed in outline Type 1 format, with associated TeX (TFM), Adobe (AFM), and Microsoft (PFM) font metrics. It should be usable with any modern LaTeX distribution and many other typesetting or word processing software. I also provide the FontForge SFD source, so you can convert it to any other format supported by FontForge.
The TeX metric file, LaTeX companion package, and dvips map file should work on any modern LaTeX distribution. I tested it on teTeX on Fedora Core 4 GNU/Linux.
If you use LTLFonts successfully on other platforms, please let me know. Once I get enough positive reports, I will be able to update this section with confidence.
LTLFonts is released under the SIL Open Font License – please read it carefully and do not download the fonts unless you agree to the terms of the license:
This Font Software is Copyright (c) 2006–2007, Matteo Slanina (http://theory.stanford.edu/~matteo/ltlfonts/). All Rights Reserved.
“LTLFonts” is a Reserved Font Name for this Font Software.
This Font Software is licensed under the SIL Open Font License, Version 1.0. No modification of the license is permitted, only verbatim copy is allowed. This license is copied below, and is also available with a FAQ at: http://scripts.sil.org/OFL
Version 1.0 – 22 November 2005
The goals of the Open Font License (OFL) are to stimulate worldwide development of cooperative font projects, to support the font creation efforts of academic and linguistic communities, and to provide an open framework in which fonts may be shared and improved in partnership with others.
The OFL allows the licensed fonts to be used, studied, modified and redistributed freely as long as they are not sold by themselves. The fonts, including any derivative works, can be bundled, embedded, redistributed and sold with any software provided that the font names of derivative works are changed. The fonts and derivatives, however, cannot be released under any other type of license.
“Font Software” refers to any and all of the following:
“Reserved Font Name” refers to the Font Software name as seen by users and any other names as specified after the copyright statement.
“Standard Version” refers to the collection of Font Software components as distributed by the Copyright Holder.
“Modified Version” refers to any derivative font software made by adding to, deleting, or substituting – in part or in whole – any of the components of the Standard Version, by changing formats or by porting the Font Software to a new environment.
“Author” refers to any designer, engineer, programmer, technical writer or other person who contributed to the Font Software.
Permission is hereby granted, free of charge, to any person obtaining a copy of the Font Software, to use, study, copy, merge, embed, modify, redistribute, and sell modified and unmodified copies of the Font Software, subject to the following conditions:
1) Neither the Font Software nor any of its individual components, in Standard or Modified Versions, may be sold by itself.
2) Standard or Modified Versions of the Font Software may be bundled, redistributed and sold with any software, provided that each copy contains the above copyright notice and this license. These can be included either as stand-alone text files, human-readable headers or in the appropriate machine-readable metadata fields within text or binary files as long as those fields can be easily viewed by the user.
3) No Modified Version of the Font Software may use the Reserved Font Name(s), in part or in whole, unless explicit written permission is granted by the Copyright Holder. This restriction applies to all references stored in the Font Software, such as the font menu name and other font description fields, which are used to differentiate the font from others.
4) The name(s) of the Copyright Holder or the Author(s) of the Font Software shall not be used to promote, endorse or advertise any Modified Version, except to acknowledge the contribution(s) of the Copyright Holder and the Author(s) or with their explicit written permission.
5) The Font Software, modified or unmodified, in part or in whole, must be distributed using this license, and may not be distributed under any other license.
This license becomes null and void if any of the above conditions are not met.
THE FONT SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE FONT SOFTWARE.
Please make sure that you read and agree with the license before you proceed.
LTLFonts is available as a compressed archive in several formats. Choose your favorite; the content is the same for all.
If you don't care and just want it to work, drop all the files from all subdirectories of the distribution in the same directory as your LaTeX document. That should do it. See the documentation section on how to use the fonts in your document.
Most likely you will want to install the fonts in a common directory in TeX's search path, so you can use it in multiple documents. This is not the place to explain how to do that, so please don't ask. Here are a few websites and book chapters to start from if you want to learn:
If you know the stuff, there should be no surprise in the LTLFonts distribution: you'll find the usual fd, tfm, pfm, pfb, and map files; just put them in the proper places.
Try this document:
% File ltlfonts-quickstart.ltx \documentclass{article} \usepackage{ltlfonts} \begin{document} LTLFonts provides some nice boxes and circles. For example: $\LTLsquare \LTLdiamond \LTLcircle a$, $\LTLcircleminus \LTLdiamondminus \LTLsquareminus \LTLcircletilde b$, $\LTLsquarehat \LTLdiamondminushat c$ \end{document}
If everything is installed correctly, you should be able to just run
latex ltlfonts-quickstart.ltx dvips -u +ltlfonts.map ltlfonts-quickstart.dvi
and get this PDF.
If you want to avoid the -u
option, you can add the
line
p +ltlfonts.map
to your .dvipsrc
.
The complete documentation is available in a PDF document, also included in the distribution.
The proof sheet, also contained in the distribution, shows more use of the font. Its LaTeX source is a good example of how to use LTLFonts to get all the LTL symbols.
If you have any comments on LTLFonts, or suggestions for improvement, please email me at matteo@cs.stanford.edu.
Currently, I would especially like to hear about:
A: You are using Windows and a version of LTLFonts prior to 0.1.2, and so you are missing the PFM metric file. Upgrade to the latest version.