Translating Higher

# Translating Higher
##### Order Problems to First-Order Clauses - Jia Meng & Lawrence C Paulson

## 
### Page 2 @ 08 April 2023 11:53:24 AM
*The main difference is that HOL terms can denote truth values and functions.*

---
and quantify over predicates?

### Page 2 @ 08 April 2023 11:55:22 AM
*combinators I, K, C, B and S*

---
undoubtedly well-known, but not to me

### Page 3 @ 08 April 2023 12:04:39 PM
*arities,*

---
!

### Page 4 @ 08 April 2023 12:10:51 PM
*Hurd [Hur03] uses an untyped translation for the same reason. No term or predicate has any type information. Because this translation can produce unsound proofs, Hurd relies on proof reconstruction to verify them. If reconstruction fails, Hurd calls the ATP again, using a typed translation. Hurd says that this happens less than one percent of the time. This combination of an efficient but unsound translation with a soundness check achieves both efficiency and soundness. We intend to take the same approach.*



id: 636279b150fe4e2e9df784e8870706ed
parent_id: 3fd5b4a78a2747a58d2c47cba81ebd67
created_time: 2023-04-15T16:58:26.879Z
updated_time: 2023-04-15T16:58:26.879Z
is_conflict: 0
latitude: 0.00000000
longitude: 0.00000000
altitude: 0.0000
author: 
source_url: 
is_todo: 0
todo_due: 0
todo_completed: 0
source: joplin-desktop
source_application: net.cozic.joplin-desktop
application_data: 
order: 1681577906879
user_created_time: 2023-04-15T16:58:26.879Z
user_updated_time: 2023-04-15T16:58:26.879Z
encryption_cipher_text: 
encryption_applied: 0
markup_language: 1
is_shared: 0
share_id: 
conflict_original_id: 
master_key_id: 
type_: 1