The paper focuses on extending existing decision procedures for set theory and related theories commonly used in mathematics to handle such notions as monotonicity, ordering, inverse functions, etc. The proposed technique is based on a syntactic translation of formulas with such special function and predicate symbols into the pure set-theoretic logic decidable by the existing decision procedures. The result can be quite useful for tool developers who aim at common mathematical reasoning.
Decision procedures for elementary sublanguages of set theory. XVII. Commonly occurring extensions of multi-level syllogistic
CANTONE, Domenico
2013-01-01
Abstract
The paper focuses on extending existing decision procedures for set theory and related theories commonly used in mathematics to handle such notions as monotonicity, ordering, inverse functions, etc. The proposed technique is based on a syntactic translation of formulas with such special function and predicate symbols into the pure set-theoretic logic decidable by the existing decision procedures. The result can be quite useful for tool developers who aim at common mathematical reasoning.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
