Predicate Logic with Definitions
<|reference_start|>Predicate Logic with Definitions: Predicate Logic with Definitions (PLD or D-logic) is a modification of first-order logic intended mostly for practical formalization of mathematics. The main syntactic constructs of D-logic are terms, formulas and definitions. A definition is a definition of variables, a definition of constants, or a composite definition (D-logic has also abbreviation definitions called abbreviations). Definitions can be used inside terms and formulas. This possibility alleviates introducing new quantifier-like names. Composite definitions allow constructing new definitions from existing ones.<|reference_end|>
@article{makarov1999predicate,
    title={Predicate Logic with Definitions},
    author={Victor Makarov},
    journal={arXiv preprint arXiv:cs/9906010},
    year={1999},
    archivePrefix={arXiv},
    eprint={cs/9906010},
    primaryClass={cs.LO cs.AI}
}