Quantifiers in logic and proof-search using permissive-nominal terms and sets

Murdoch J. Gabbay; Claus-Peter Wirth

doi:10.1093/logcom/exs057

Quantifiers in logic and proof-search using permissive-nominal terms and sets

Murdoch J. Gabbay^*, Claus-Peter Wirth

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

Abstract

We investigate models of first-order logic designed to give semantics to reductive proof-search systems, with special attention to the so-called gamma- and delta-rules controlling quantifiers. The key innovation is the use of syntax and semantics with (finitely supported) name-symmetry, in the style of nominal techniques.

Original language	English
Pages (from-to)	473-523
Number of pages	51
Journal	Journal of Logic and Computation
Volume	25
Issue number	2
Early online date	23 Feb 2013
DOIs	https://doi.org/10.1093/logcom/exs057
Publication status	Published - Apr 2015

Keywords

proof-search
nominal techniques
name-symmetry
higher-order logic
quantifiers
CAPTURE-AVOIDING SUBSTITUTION
VARIABLE SEMANTIC TABLEAUX
DELTA-RULE
UNIFICATION
ALGEBRA
INFINITE
BINDING
NAMES

Access to Document

10.1093/logcom/exs057

Cite this

@article{d10d3402a08d491aae644d6e0d43abfa,

title = "Quantifiers in logic and proof-search using permissive-nominal terms and sets",

abstract = "We investigate models of first-order logic designed to give semantics to reductive proof-search systems, with special attention to the so-called gamma- and delta-rules controlling quantifiers. The key innovation is the use of syntax and semantics with (finitely supported) name-symmetry, in the style of nominal techniques.",

keywords = "proof-search, nominal techniques, name-symmetry, higher-order logic, quantifiers, CAPTURE-AVOIDING SUBSTITUTION, VARIABLE SEMANTIC TABLEAUX, DELTA-RULE, UNIFICATION, ALGEBRA, INFINITE, BINDING, NAMES",

author = "Gabbay, {Murdoch J.} and Claus-Peter Wirth",

year = "2015",

month = apr,

doi = "10.1093/logcom/exs057",

language = "English",

volume = "25",

pages = "473--523",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press",

number = "2",

}

TY - JOUR

T1 - Quantifiers in logic and proof-search using permissive-nominal terms and sets

AU - Gabbay, Murdoch J.

AU - Wirth, Claus-Peter

PY - 2015/4

Y1 - 2015/4

N2 - We investigate models of first-order logic designed to give semantics to reductive proof-search systems, with special attention to the so-called gamma- and delta-rules controlling quantifiers. The key innovation is the use of syntax and semantics with (finitely supported) name-symmetry, in the style of nominal techniques.

AB - We investigate models of first-order logic designed to give semantics to reductive proof-search systems, with special attention to the so-called gamma- and delta-rules controlling quantifiers. The key innovation is the use of syntax and semantics with (finitely supported) name-symmetry, in the style of nominal techniques.

KW - proof-search

KW - nominal techniques

KW - name-symmetry

KW - higher-order logic

KW - quantifiers

KW - CAPTURE-AVOIDING SUBSTITUTION

KW - VARIABLE SEMANTIC TABLEAUX

KW - DELTA-RULE

KW - UNIFICATION

KW - ALGEBRA

KW - INFINITE

KW - BINDING

KW - NAMES

U2 - 10.1093/logcom/exs057

DO - 10.1093/logcom/exs057

M3 - Article

SN - 0955-792X

VL - 25

SP - 473

EP - 523

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 2

ER -

Quantifiers in logic and proof-search using permissive-nominal terms and sets

Abstract

Keywords

Access to Document

Fingerprint

Cite this