Questions tagged [first-order-logic]
The first-order-logic tag has no usage guidance.
6
questions
0
votes
2
answers
184
views
What is the meta-language of ZFC?
This is a good post which says that all proof assistants are founded in HOL, first order logic, or dependent types.
Does this mean that the axioms of ZFC are just expressions obtainable from the ...
- 157
0
votes
1
answer
61
views
Can alg be used for the formal semantics of a language?
This library “generates all models of a first order theory”: https://github.com/andrejbauer/alg
Is it able to take the formal semantics of a programming language, like:
x86: https://dl.acm.org/doi/10....
- 157
0
votes
1
answer
55
views
Why doesn't the `div` predicate work here?
(declare-fun pdiv (Int Int Int) Bool)
(assert (forall ((x Int) (y Int) (z Int)) (=> (= z (div x y)) (pdiv z x y))))
When I check sat, I've got unknown by Z3
- 11
5
votes
1
answer
149
views
Is ACL2 first-order-logic and is this a limitation for proving math?
I am considering whether I should learn the ACL2 proof assistant. However, before diving into that, I wanted to know if there are significant limitations in terms of proving math. The first thing I ...
- 1,608
1
vote
2
answers
158
views
Does quantification over functions (STLC) increase strength beyond first order logic?
Does quantification over functions (STLC) increase strength beyond first order logic?
I want to add support for binders in my little constructive first order logic formalism I'm working on but I'm ...
- 2,748
4
votes
3
answers
628
views
Creating a proof assistant for first order logic in Haskell
I am planning to implement a FOL proof assistant in Haskell. What are some useful libraries and implementations I should be looking at?
Here are some further details. I have a simple proof checker for ...
- 419