JAR
2010
13 years 6 months ago
2010
Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves ...
JAR
2010
13 years 6 months ago
2010
This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first prove the existence of an ide...
JAR
2010
13 years 6 months ago
2010
Based on inductive definitions, we develop a tool that automates the definition of partial recursive functions in higher-order logic (HOL) and provides appropriate proof rules for ...
JAR
2010
13 years 6 months ago
2010
The development of ontologies involves continuous but relatively small modifications. However, existing ontology reasoners do not take advantage of the similarities between differe...
JAR
2010
13 years 10 months ago
2010
JAR
2010
13 years 10 months ago
2010
Meta-logics and type systems based on intuitionistic logic are commonly used for specifying natural deduction proof systems. We shall show here that linear logic can be used as a m...
JAR
2010
13 years 10 months ago
2010
Many theorems involving special functions such as ln, exp and sin can be proved automatically by MetiTarski: a resolution theorem prover modified to call a decision procedure for ...
JAR
2010
13 years 10 months ago
2010
Abstract. We present a declarative language inspired by the pseudonatural language used in Matita for the explanation of proof terms. We show how to compile the language to proof t...