commit e309cbad69a3fd846ed20abb2bbfbc3322420cb2
Author: Christian Ohlsson <crille@crille.org>
Date:   Thu Mar 5 13:42:07 2026 +0100

    Startpunkten

diff --git a/Free_In_and_Rename_Var/lab2.pl b/Free_In_and_Rename_Var/lab2.pl
new file mode 100644
index 0000000..ffa2eeb
--- /dev/null
+++ b/Free_In_and_Rename_Var/lab2.pl
@@ -0,0 +1,47 @@
+/*****************************/
+/* Christian Ohlsson         */
+/* Logik för dataloger       */
+/* Karlstad 990228           */
+/* Laboration 2 i Logik      */
+/*****************************/
+/* Functions included        */
+/* free_in                   */
+/* rename_var                */
+/*****************************/
+
+:- op(200, fx, -).
+:- op(400, xfy, #).
+:- op(400, xfy, &).
+:- op(700, xfy, ->).
+:- op(700, xfy, <->).
+
+exist(X, [H|T]) :- X = H, !, fail.
+exist(X, [H|T]) :- Z =.. T, free_in(X, Z).
+
+all(X, [H|T]) :- X = H, !, fail.
+all(X, [H|T]) :- Z =.. T, free_in(X, Z).
+
+operators(X, [H|T]) :- free_in(X, H), Z =.. T, free_in(X, Z).
+falsum(X) :- true.
+
+/* Del 1 - free_in */
+/* free_in(+variabel, +TermOrFormula */
+free_in(X, Y) :- Y =.. [H|T], T = [].
+
+free_in(X, Y) :- Y =.. [H|T], member(H, [&, #, ->, <->]), operators(X, T).
+free_in(X, Y) :- Y =.. [H|T], member(H, [all, exist]), call(H, X, T).
+free_in(X, Y) :- Y =.. [H|T], member(H, [-]), falsum(X).
+free_in(X, Y) :- Y =.. [H|T], member(H, [as, pr, fu, qu, rt]).
+
+/* Del 2 - rename_var  */
+/* rename_var(+Element, +TermOrFormula, +Nyttelement, -NyTermOrFormula) */
+ersatt(E1, E2, [], []).
+ersatt(E1, E2, [E1|R], [E2|S]) :- ersatt(E1, E2, R, S).
+ersatt(E1, E2, [X|R], [X|S]) :- ersatt(E1, E2, R, S).
+
+
+rv(E1, E2, [H|T], New) :- T = [], atom(H), ersatt(E1, E2, [H], New).
+rv(E1, E2, [H|T], New) :- T = [], rename_var(E1, H, E2, Next), append([Next], [], New).
+rv(E1, E2, [H|T], New) :- rv(E1, E2, T, N1), rv(E1, E2, [H], N2), append(N2,N1, New).
+rename_var(E1, Old, E2, New) :- Old =.. [H|T], T = [], ersatt(E1, E2, [H], Z), New =.. Z. 
+rename_var(E1, Old, E2, New) :- Old =.. [H|T], rv(E1, E2, T, Next), New =.. [H|Next].
diff --git a/Prenex_Normal_Form/lab3.pl b/Prenex_Normal_Form/lab3.pl
new file mode 100644
index 0000000..eb19c75
--- /dev/null
+++ b/Prenex_Normal_Form/lab3.pl
@@ -0,0 +1,219 @@
+/*****************************/
+/* Christian Ohlsson         */
+/* Logik för dataloger       */
+/* Karlstad 990228           */
+/* Laboration 3 i Logik      */
+/*****************************/
+/* Functions included        */
+/* prenex                    */
+/* implout                   */
+/* negin                     */
+/* kvant                     */
+/* free_in                   */
+/* rename_var                */
+/*****************************/  
+
+:- op(200,fx,~).
+:- op(400,xfy,#).
+:- op(400,xfy,&).
+:- op(700,xfy,->).
+:- op(700,xfy,<->).               
+
+prenex(Formel,PNF):-
+	implout(Formel,Svar1),
+	negin(Svar1,Svar2),
+	kvant(Svar2,PNF,[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10],L).
+
+/* *****************************   IMPLOUT   **************************** */  
+
+implout((P<->Q),((P1&Q1)#(~P1&~Q1))) :- !,implout(P,P1),implout(Q,Q1).
+implout((P->Q),(~P1#Q1)) :- !,implout(P,P1),implout(Q,Q1).
+implout(all(X,P),all(X,P1)) :- !,implout(P,P1).
+implout(exist(X,P),exist(X,P1)) :- !,implout(P,P1).
+implout((P&Q),(P1&Q1)) :- !,implout(P,P1),implout(Q,Q1).
+implout((P#Q),(P1#Q1)) :- !,implout(P,P1),implout(Q,Q1).
+implout((~P),(~P1)) :- !,implout(P,P1).
+implout(P,P).                           
+
+/* *****************************   NEGIN   **************************** */ 
+
+negin((~P),P1) :- !,neg(P,P1).
+negin(all(X,P),all(X,P1)) :- !,negin(P,P1).
+negin(exist(X,P),exist(X,P1)) :- !,negin(P,P1).
+negin((P&Q),(P1&Q1)) :- !,negin(P,P1),negin(Q,Q1).
+negin((P#Q),(P1#Q1)) :- !,negin(P,P1),negin(Q,Q1).
+negin(P,P).
+neg((~P),P1) :- !,negin(P,P1).
+neg(all(X,P),exist(X,P1)) :- !,neg(P,P1).
+neg(exist(X,P),all(X,P1)) :- !,neg(P,P1).
+neg((P&Q),(P1#Q1)) :- !,neg(P,P1),neg(Q,Q1).
+neg((P#Q),(P1&Q1)) :- !,neg(P,P1),neg(Q,Q1).
+neg(P,(~P)).             
+                        
+/* *****************************   RENAME-VAR   **************************** */ 
+
+r_v(X,exist(X,P),exist(F,P1),[F|R]):- r_v(X,P,P1,[F|R]).
+r_v(X,exist(Y,P),exist(Y,P1),[F|R]):-  X\==Y, r_v(X,P,P1,[F|R]).
+
+r_v(X,all(X,P),all(F,P1),[F|R]):- r_v(X,P,P1,[F|R]).
+r_v(X,all(Y,P),all(Y,P1),[F|R]):-  X\==Y, r_v(X,P,P1,[F|R]).
+
+r_v(X,Y#Z,Y1#Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
+r_v(X,Y&Z,Y1&Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]). 
+r_v(X,Y->Z,Y1->Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
+r_v(X,Y<->Z,Y1<->Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
+
+r_v(X,Y,Y2,[F|R]):- Y=..[T,S],r_v(X,S,Y1,[F|R]), Y2=..[T,Y1].
+r_v(X,[T|S],[F|S1],[F|R]):- X==T, r_v(X,S,S1,[F|R]).
+r_v(X,[T|S],[S2|S1],[F|R]):- X\==T, r_v(X,S,S1,[F|R]),r_v(X,T,S2,[F|R]).
+r_v(X,~P,~P1,[F|R]):- r_v(X,P,P1,[F|R]).
+r_v(X,X,F,[F|R]).
+r_v(X,U,U,[F|R]):- X\==U.
+    
+/* *****************************   FREE   ****************************** */ 
+
+free_in(X,exist(Y,P)):- X\==Y, free_in(X,P).
+free_in(X,all(Y,P)):- X\==Y, free_in(X,P).
+free_in(X,Y#Z):-free_in(X,Y);free_in(X,Z).
+free_in(X,Y&Z):-free_in(X,Y);free_in(X,Z).
+free_in(X,Y->Z):-free_in(X,Y);free_in(X,Z).
+free_in(X,Y<->Z):-free_in(X,Y);free_in(X,Z).
+
+free_in(X,Y):- Y=..[F,R],free_in(X,R).
+free_in(X,[F|R]):-free_in(X,F);free_in(X,R).
+
+free_in(X,~Z):-free_in(X,Z).
+free_in(X,X).
+                              
+
+/* ********************************************************************* */ 
+/* *****************************   ALL &   ***************************** */ 
+
+kvant(all(X,Y)&Z,SY,[F|R],L3):-   
+	(free_in(X,Z),
+	r_v(X,Z,Z1,[F]),
+	kvant(Y,Y1,R,R1),
+	kvant(Z1,Z2,R1,L2),
+       kvant(all(X,(Y1&Z2)),SY,L2,L3));
+        	(kvant(Y,Y1,R,R1),
+                kvant(Z,Z2,R1,L2),
+                kvant(all(X,(Y1&Z2)),SY,L2,L3)).  
+                          
+/* *****************************   & ALL   **************************** */ 
+
+kvant(Z&all(X,Y),SY,[F|R],L3):-   
+	(free_in(X,Z),
+       r_v(X,Z,Z1,[F]),
+	kvant(Y,Y1,R,R1),
+	kvant(Z1,Z2,R1,L2),
+       kvant(all(X,(Z2&Y1)),SY,L2,L3));
+        	(kvant(Y,Y1,R,R1),
+                kvant(Z,Z2,R1,L2),
+                kvant(all(X,(Z2&Y1)),SY,L2,L3)).  
+ 
+
+/* *****************************   ALL #   **************************** */ 
+
+kvant(all(X,Y)#Z,SY,[F|R],L3):-   
+	(free_in(X,Z),
+        r_v(X,Z,Z1,[F]),
+	kvant(Y,Y1,R,R1),
+	kvant(Z1,Z2,R1,L2),
+        kvant(all(X,(Y1#Z2)),SY,L2,L3));
+        	(kvant(Y,Y1,R,R1),
+                kvant(Z,Z2,R1,L2),
+                kvant(all(X,(Y1#Z2)),SY,L2,L3)).  
+
+                                             
+/* *****************************   # ALL   **************************** */ 
+
+kvant(Z#all(X,Y),SY,[F|R],L3):-   
+	(free_in(X,Z),
+       r_v(X,Z,Z1,[F]),
+	kvant(Y,Y1,R,R1),
+	kvant(Z1,Z2,R1,L2),
+       kvant(all(X,(Z2#Y1)),SY,L2,L3));
+        	(kvant(Y,Y1,R,R1),
+                kvant(Z,Z2,R1,L2),
+                kvant(all(X,(Z2#Y1)),SY,L2,L3)). 
+ 
+
+/* ***************************   EXIST &   ************************** */ 
+
+kvant(exist(X,Y)&Z,SY,[F|R],L3):-   
+	(free_in(X,Z),
+       r_v(X,Z,Z1,[F]),
+	kvant(Y,Y1,R,R1),
+	kvant(Z1,Z2,R1,L2),
+       kvant(exist(X,(Y1&Z2)),SY,L2,L3));
+        	(kvant(Y,Y1,R,R1),
+                kvant(Z,Z2,R1,L2),
+                kvant(exist(X,(Y1&Z2)),SY,L2,L3)).  
+   
+/* ***************************   & EXIST   ************************** */ 
+
+kvant(Z&exist(X,Y),SY,[F|R],L3):-   
+	(free_in(X,Z),
+       r_v(X,Z,Z1,[F]),
+	kvant(Y,Y1,R,R1),
+	kvant(Z1,Z2,R1,L2),
+       kvant(exist(X,(Z2&Y1)),SY,L2,L3));
+        	(kvant(Y,Y1,R,R1),
+                kvant(Z,Z2,R1,L2),
+                kvant(exist(X,(Z2&Y1)),SY,L2,L3)).  
+   
+/* ***************************   EXIST #   ************************** */ 
+
+kvant(exist(X,Y)#Z,SY,[F|R],L3):-   
+	(free_in(X,Z),
+	r_v(X,Z,Z1,[F]),
+	kvant(Y,Y1,R,R1),
+	kvant(Z1,Z2,R1,L2),
+       kvant(exist(X,(Y1#Z2)),SY,L2,L3));
+        	(kvant(Y,Y1,R,R1),
+                kvant(Z,Z2,R1,L2),
+                kvant(exist(X,(Y1#Z2)),SY,L2,L3)).
+       
+/* ***************************   # EXIST   ************************** */ 
+
+kvant(Z#exist(X,Y),SY,[F|R],L3):-   
+	(free_in(X,Z),
+	r_v(X,Z,Z1,[F]),
+	kvant(Y,Y1,R,R1),
+	kvant(Z1,Z2,R1,L2),
+       kvant(exist(X,(Z2#Y1)),SY,L2,L3));
+        	(kvant(Y,Y1,R,R1),
+                kvant(Z,Z2,R1,L2),
+                kvant(exist(X,(Z2#Y1)),SY,L2,L3)). 
+ 
+
+
+/* ***************************     &       ************************** */ 
+
+kvant(P&Q,PQ,L,L3):-
+      kvant(P,P1,L,L1),
+      kvant(Q,Q1,L1,L2),
+      ((P1\==P);(Q1\==Q)),
+      kvant(P1&Q1,PQ,L2,L3).
+ 
+/* ***************************     #       ************************** */ 
+
+kvant(P#Q,PQ,L,L3):-
+      kvant(P,P1,L,L1),
+      kvant(Q,Q1,L1,L2),
+      ((P1\==P);(Q1\==Q)),
+      kvant(P1#Q1,PQ,L2,L3).
+
+/* ***************************    EXIST   ************************** */ 
+
+kvant(all(X,F),all(X,F1),L1,L2):-
+       kvant(F,F1,L1,L2).
+       
+/* ***************************   ALL        ************************** */ 
+
+kvant(exist(X,F),exist(X,F1),L1,L2):-
+       kvant(F,F1,L1,L2).
+
+/* ***************************   BASFALL    ************************** */ 
+
+kvant(X,X,L,L).
diff --git a/Prolog_Intro/lab1.pl b/Prolog_Intro/lab1.pl
new file mode 100644
index 0000000..95bf309
--- /dev/null
+++ b/Prolog_Intro/lab1.pl
@@ -0,0 +1,150 @@
+/*****************************/
+/* Christian Ohlsson         */
+/* Logik för dataloger       */
+/* Karlstad 990228           */
+/* Lab 1 i Logik             */
+/*****************************/
+/* Functions included:       */
+/*   smaller_than_all        */
+/*   exchange_all            */
+/*   exchange_nth            */
+/*   subset                  */
+/*   member                  */
+/*****************************/
+/*   sum                     */
+/*   product                 */
+/*   fac                     */
+/*****************************/
+/*   diff                    */
+/*   ismother                */
+/*   isfather                */
+/*   isson                   */
+/*   sisterof                */
+/*   grandpaof               */
+/*   sibling                 */
+/*****************************/
+
+/******************************************************
+   smaller_than_all (M, [array of numbers]).
+   Kollar om M är mindre än alla tal i arrayen
+   och om så är fallet svarar kompilatorn med Yes
+*/
+smaller_than_all(M,[]).
+smaller_than_all(M,[Y|L]) :- M < Y, smaller_than_all(M, L).
+
+/******************************************************
+   exchange_all(E1,E2,[indata-array],[utdata-array])
+   Byter ut alla E1 mot E2 i indata-arrayen
+   och lagrar detta i utdata-arrayen
+*/
+exchange_all(E1,E2,[],[]).
+exchange_all(E1,E2,[Y|L], [F|R]):-E1 = Y, F is E2,exchange_all(E1,E2,L,R).
+exchange_all(E1,E2,[Y|L], [Y|R]):-exchange_all(E1,E2,L,R). 
+
+/******************************************************
+   exchange_nth(E1,E2,[indata-array],[utdata-array])
+   Byter ut elementet på plats E1 mot E2
+*/
+exchange_nth(E1,E2,[],[]).
+exchange_nth(E1,E2,[Y|L],[F|R]):-E1 = 1,F is E2, exchange_nth(0,E2,L,R).
+exchange_nth(E1,E2,[Y|L], [Y|R]):-W is E1-1,exchange_nth(W,E2,L,R).
+
+/******************************************************
+   subset([array1], [array2])
+   Kollar om alla element i array1 finns med
+   i array2 och returnerar då Yes.
+*/
+subset([], L).
+subset([Y|L], R):- member(Y, R),subset(L,R).
+
+member(X,[X|_]).
+member(X,[_|Y]):-member(X,Y).
+
+/******************************************************
+  sum
+    Tar emot tre värden och svarar 
+    Yes om det tredje värdet är summan av 
+    de två tidigare.
+  product
+    Tar emot tre värden och svarar 
+    Yes om det tredje värdet är produkten 
+    av de två tidigare.
+  fac
+    Tar emot två värden och svarar 
+    Yes om det andra värdet är faculteten 
+    av det första.
+*/
+sum(N, N1, S) :- S is N + N1.
+product(N1, N2, S) :- S is N1 * N2.
+fac(1,1).
+fac(N, S) :- M is N-1, fac(M, Z), S is N * Z.
+
+/******************************************************
+  Familjen
+*/
+/* Män */
+male(martin).
+male(olle).
+male(pelle).
+male(peter).
+male(stefan).
+male(tadek).
+male(sven).
+
+/* Kvinnor */
+female(anna).
+female(claudia).
+female(edyta).
+female(terry).
+female(berit).
+female(halina).
+
+/* parents(X, Y, Z) = Z, Y föräldrar till X */
+parents(anna, berit, stefan).
+parents(martin, berit, stefan).
+parents(edyta, halina, tadek).
+parents(peter, halina, tadek).
+
+/* father(X, Y) = X är far till Y */
+father(stefan, anna).
+father(sven, tadek).
+father(stefan, martin).
+father(tadek, edyta).
+father(tadek, peter).
+
+/* mother(X, Y) = X är mor till Y */
+mother(berit, anna).
+mother(berit, martin).
+mother(halina, edyta).
+mother(halina, peter).
+
+/* parent(X, Y) = X är förälder till Y */
+parent(berit, anna).
+parent(berit, martin).
+parent(stefan, anna).
+parent(stefan, martin).
+parent(halina, edyta).
+parent(halina, peter).
+parent(tadek, edyta).
+parent(tadek, peter).
+
+/* diff(X, Y) = X är inte densamma som Y */
+diff(X, Y) :- X \= Y.
+
+/* ismother(X) = X är en mor */
+ismother(X) :- parents(_, X, _), female(X).
+
+/* isfather(X) = X är en far */
+isfather(X) :- parents(_, _, X), male(X).
+
+/* isson(X) = X är en son */
+isson(X)   :- parents(X, _, _), male(X).
+
+/* sisterof(X, Y) = X är syster till Y */
+sisterof(X, Y) :- female(X), parents(X,_,_), parents(Y,_,_), diff(X, Y).
+
+/* grandpaof(X, Y) = X är grandpa till Y */
+grandpaof(X, Y) :- male(X), father(X, FF), parents(Y, _, FF).
+
+/* sibling(X, Y) = X och Y är syskon */
+sibling(X, Y) :- parents(X, _, F), parents(Y, _, F), diff(X, Y).