Stack Overflow
Stack Overflow

Questions tagged [propositional-calculus]

29 questions
9
votes
3 answers

Prolog implementation of Quine's algorithm for classical propositional logic (in Quine's "Methods of Logic")

I know only one prover that translates the algorithm that Quine gave for classical propositional logic in his book Methods of Logic (Harvard University Press, 1982, ch. 1 sec. 5, pp. 33-40), this prover is in Haskell and it is here: Quine's…
Joseph Vidal-Rosset
  • 137
  • 1
  • 10
7
votes
1 answer

Lowering infix operator precedence in R?

I'm trying to make an 'implies' operator for logical variables in R to make propositional calculus easier. However it doesn't seem to be playing nice with the negation operator. As the last 4 lines here indicate, I have to wrap negated variables in…
BBrooklyn
  • 350
  • 1
  • 3
  • 15
2
votes
1 answer

How to determine if two propositional formulas are equivalent in Prolog?

I'm new to Prolog and have some doubts. I need to write a function form_equiv(A,B) that tells us if if B is equivalent to A where A and B are supposed to be propositions. I know that two propositions are equivalent if tautology (A iff B) = TRUE But…
Massimo2015MX
  • 65
  • 5
2
votes
2 answers

Coq: a vicious circle with two identical subgoals

Sorry for overcomplicated example. I have Lemma test : forall x y z : Prop, ( (((x → (y ∨ z)) → (x ∨ y)) ↔ (x ∨ y)) ∧ (((y → (x ∨ z)) → (x ∨ y)) ↔ (x ∨ y)) ∧ ((y → (x ∨ z)) → (x ∨ (x → (y ∨ z)))) ∧ ((x → (y ∨ z)) → (y ∨ (y → (x ∨…
მამუკა ჯიბლაძე
  • 187
  • 3
  • 9
2
votes
2 answers

Quine's algorithm with Single Sided Unification in Prolog

The new release 8.3.19 of SWI-Prolog introduces single sided unification inside new Picat style rules. This could be a welcome addition to any Prolog system. I was wondering whether we could rewrite Quine algorithm Prolog implementation of Quine's…
user502187
2
votes
2 answers

Generating unsatisfiable test problems

I'm trying to generate some test problems for propositional satisfiability, in particular to generate some that are unsatisfiable, but according to a fixed pattern, so that for any N, an unsatisfiable problem of N variables can be generated. An easy…
rwallace
  • 31,405
  • 40
  • 123
  • 242
2
votes
1 answer

Transitivity, or How To Chain Generic Implicits in Scala

I'm attempting to extend the functionality described in this excellent article by Miles Sabin: Unboxed Union Types to support n-ary type unions, e.g.: def if[T](t: T)(implicit ev: T <<: (Int | String | Symbol | Double)): String = ??? I've modified…
wvandaal
  • 4,265
  • 2
  • 16
  • 27
2
votes
1 answer

Given n boolean variables, how to check if k or less of them are true only by means of propositional calculus?

During my assignments for theoretical CS I stumbled over the questions how a boolean function would look, that tests if of n given boolean vars, x1 to xn, k or less variables are true. In Java this would be fairly simple : public boolean…
Lennart F
  • 21
  • 2
1
vote
3 answers

Python - join propositions

I have an list of strings which illustrate propositions. E.g. L = ['(A∧B)', 'A', 'B'] My aim is to join each element with the string '∧' and brackets "()", which results in following string: aim = "(((A ∧ B) ∧ A) ∧ B)" is their a simple method to…
Martin Kunze
  • 995
  • 6
  • 16
1
vote
0 answers

Lean : Proof that \ not p \to (p \ to q) or similar false \to p

I am new at lean - prover and I am trying to solve the examples on the online tutorial. I am stuck at this example and I need to prove that "false implies q" or something like that. My code is : variables p q : Prop example : ¬ p → (p → q) := …
Georgios Papanikolaou
  • 21
  • 4
1
vote
1 answer

Recursive Descent Parser Should Error on Repetitive Letter Terminals

Primary question: How can I update my recursive descent parser for propositional logic (written in JavaScript) so that strings like "p~" and "pp" will return an "Invalid" message? I am very new to HTML, JavaScript, and parsing. I wanted to see if I…
Zachary
  • 27
  • 7
0
votes
1 answer

Express each of these statements in terms of C(x), D(x), F(x), quantifiers, and logical connectives

Let C(x) be the statement “x has a cat,” let D(x) be the statement “x has a dog,” let F(x) be the statement “x has a ferret.” Express each of these statements in terms of C(x), D(x), F(x), quantifiers, and logical connectives. Q1. For each of the…
سہیل احمد
  • 1
0
votes
2 answers

Max of a list of vectors of Boolean using z3 for resolution of SAT problem

I am working on a Sat project, one of my subtasks is to compute the max of a list of a vectors of boolean, each of them is a number. An example of the vector is [False,True,True,False], it represents the number 2^2 + 2^1 = 6. In this resolution I…
jacopodabramo
  • 15
  • 4
0
votes
0 answers

Branching out of recursive function

I've been trying to write a program to check whether a propositional logic formula is valid or not by representing it as a tree and then recursively negating the root node and all subtrees appropriately to look for contradictions, and I reached a…
Matheus
  • 1
  • 1
0
votes
0 answers

Trying to understand the tableaux method of propositional calculus

I have been reading Raymond Smullyan's wonderful book titled Logical Labyrinths. I'm having trouble understanding the completeness proof of the Tableaux method. In order to show that a sentence X is a tautology, we show that F X results in a closed…
user2374991
  • 21
  • 1
1
2