Questions tagged [first-order-logic]
The first-order-logic tag has no usage guidance.
7
questions
3
votes
2
answers
201
views
Enumerating all formulae of any first-order language
I'm formalizing the metatheory of first-order logic with Coq.
I want to enumerate all expressions of any first-order language.
The syntax of terms and formulae are:
...
- 83
1
vote
2
answers
301
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 ...
0
votes
1
answer
65
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....
0
votes
1
answer
59
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
6
votes
1
answer
224
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 ...
- 2,220
1
vote
2
answers
173
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,868
4
votes
3
answers
823
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 ...
- 429