Questions tagged [proof-system]
8 questions
9
votes
6 answers
Interactive math proof system
I'm looking for a tool (GUI preferred but CLI would work) that allows me to input math expressions and then perform manipulations of them but restricts me to only mathematically valid operations. Also, the tool must be able to save a session and…
BCS
- 75,627
- 68
- 187
- 294
6
votes
2 answers
Relation between types prod and sig in COQ
In COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is described the fact that the cartesian product is a particular case of dependent sum? I wonder…
user1902311
5
votes
1 answer
Help with a Coq proof for SubSequences
I have the defined inductive types:
Inductive InL (A:Type) (y:A) : list A -> Prop :=
| InHead : forall xs:list A, InL y (cons y xs)
| InTail : forall (x:A) (xs:list A), InL y xs -> InL y (cons x xs).
Inductive SubSeq (A:Type) : list A -> list…
Tiago Veloso
- 8,513
- 17
- 64
- 85
3
votes
1 answer
How to automatically proof that two first-order formulas are equivalent?
What is the best way to automatically proof that two first-order formulas F and G are equivalent?
The formulas have some restrictions compared to "full" first-order formulas:
quantifier-free
function-free
implicitly universally quantified
I can…
user909998
- 153
- 6
1
vote
1 answer
Theorem Prover: How to optimize a backward proof search containing a "useless rule AND"
Quick review:
Inference rule = conclusion + rule + premises
Proof tree = conclusion + rule + sub-trees
Backward proof search: given an input goal, try to build a proof tree by applying inference rules in bottom-up way (for example, the goal is…
Marco Dinh
- 332
- 2
- 15
0
votes
3 answers
Has anybody used a proof assistant to prove soundness of a typed process calculus?
...And have they published the results where I can afford to read them?
james woodyatt
- 2,170
- 17
- 17
0
votes
1 answer
Derivation in the Resolution Proof System
The clauses of our problem: {x,y},{x,z},{y,z},{¬x,¬y},{¬x,¬z},{¬y,¬z}
How can we conclude from these clauses to {}?
I can see that this cannot be satisfied, but I am unable to find a solution in the Resolution Proof System as it seems that…
NightOwl
- 3
- 2
0
votes
2 answers
Natural deduction: is this a sound proof?
I have attempted to solve the following but I have no means to check it....or does wolfram do this ? I do not know if my handling of the operators (scope) is occrect...do you know?
for all x: upended A operator (universality)
there exists an x:…
ledawg
- 2,395
- 1
- 11
- 17