I am currently studying Fitch Format first order logic proofs. My lecturer follows closely Language, Proof and Logic by Jon Barwise. I am trying to do some proofs but I am having some trouble getting to understand how to do these proofs. As I have already read what Language Proof and Logic has to offer, I'd like to know if there are an...
Hi, Can someone validate the following. I am supposed to 'write a formula asserting that for every number there's a unique next number...true for integers for instance' L(x,y) means x is smaller than y the intended Domain is the Integer numbers Can I give x y [ x<y ( z : z<x y<z ) ] Thanks ...
Is there any software around that using the Fitch format (used in ), allows one to put a specific set of premises and goals and have it show us the full list of steps needed to solve the problem? ...
I've been using the following data structure for the representation of propositional logic in Haskell: data Prop = Pred String | Not Prop | And Prop Prop | Or Prop Prop | Impl Prop Prop | Equiv Prop Prop deriving (Eq, Ord) Any comments on this structure are welcome. However, now I want to extend ...
If I want to express in first-order logic that 'the element(s) in the set with the smallest radius has the value 0', would the following be right? e1 S. e2 S. Radius e1 Radius e2 Value e1 = 0? Are the variables correctly quantified? Thanks ...
Using only these predicates..... child(X) X is a child unwell(X,Y) X is unwell on day Y location(X,Y,Z) Location of X on day Y is Z (school, park, home) sunny(X) X is a sunny day Generally, children do not go to school whenever they are unwell ∄x [Child(x) ∧ location(X,y,home) → Child(x) ∧ unwell(X,y)] Not s...
I found a sat solver in http://code.google.com/p/aima-java/ I tried the following code to solve an expression using dpllsolver the input is (A <=> B) AND (C => D) AND (A AND C) AND (NOT (B AND D)) AND (NOT (B AND D AND E)) CNF transformer transforms it to ( ( ( NOT A ) OR B ) AND ( ( NOT B ) OR A ) ) it doesn't consider t...