Sciweavers

Share
JAR
2010
95views more  JAR 2010»
8 years 7 days ago
Equivariant Unification
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 ...
James Cheney
JAR
2010
98views more  JAR 2010»
8 years 7 days ago
Proof-Guided Test Selection from First-Order Specifications with Equality
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...
Delphine Longuet, Marc Aiguier, Pascale Le Gall
JAR
2010
122views more  JAR 2010»
8 years 7 days ago
Partial and Nested Recursive Function Definitions in Higher-order Logic
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 ...
Alexander Krauss
JAR
2010
139views more  JAR 2010»
8 years 7 days ago
Incremental Classification of Description Logics Ontologies
The development of ontologies involves continuous but relatively small modifications. However, existing ontology reasoners do not take advantage of the similarities between differe...
Bernardo Cuenca Grau, Christian Halaschek-Wiener, ...
JAR
2010
123views more  JAR 2010»
8 years 3 months ago
A Framework for Proof Systems
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...
Vivek Nigam, Dale Miller
JAR
2010
160views more  JAR 2010»
8 years 3 months ago
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions
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 ...
Behzad Akbarpour, Lawrence C. Paulson
JAR
2010
160views more  JAR 2010»
8 years 3 months ago
Declarative Representation of Proof Terms
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...
Claudio Sacerdoti Coen
books