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

Murdoch J. Gabbay, Claus-Peter Wirth

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)473-523
Number of pages51
JournalJournal of Logic and Computation
Volume25
Issue number2
Early online date23 Feb 2013
DOIs
Publication statusPublished - 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

Cite this