María Manzano. Extensions of first order logic. Cambridge tracts in theoretical computer science, no. 19. Cambridge University Press, Cambridge, New York, and Oakleigh, Victoria, 1996, xxii + 388 pp.

1998 ◽  
Vol 63 (3) ◽  
pp. 1194-1196
Author(s):  
Yde Venema
Keyword(s):  
New York ◽  
Computer Science ◽  
Theoretical Computer Science ◽  
Order Logic ◽  
First Order Logic ◽  
Theoretical Computer ◽  
Cambridge University ◽  
First Order

scholarly journals Herbrand Proofs and Expansion Proofs as Decomposed Proofs

2020 ◽  
Vol 30 (8) ◽  
pp. 1711-1742
Author(s):  
Benjamin Ralph
Keyword(s):  
Propositional Logic ◽  
Theoretical Computer Science ◽  
Order Logic ◽  
First Order Logic ◽  
System Expansion ◽  
Theoretical Computer ◽  
First Order ◽  
Deep Inference ◽  
Definition Of ◽  
Inference Systems

Abstract The reduction of undecidable first-order logic to decidable propositional logic via Herbrand’s theorem has long been of interest to theoretical computer science, with the notion of a Herbrand proof motivating the definition of expansion proofs. In this paper we construct simple deep inference systems for first-order logic, both with and without cut, such that ‘decomposed’ proofs—proofs where the contractive and non-contractive behaviour of the proof is separated—in each system correspond to either expansion proofs or Herbrand proofs. Translations between proofs in this system, expansion proofs and Herbrand proofs are given, retaining much of the structure in each direction.

Sign in / Sign up

Export Citation Format

Share Document