josejuan/microProber.html

## microProber.html
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<title>Micro Verificador de Teoremas</title>
<script src="http://code.jquery.com/jquery-1.7.2.min.js"></script>
<script>
	function MicroVerificador(reglas, consultas) {
		var w = ["siempre_que", "no", "y", "o", "implica_que", "cierto", "falso", "(", ")"];
		var clear = function(s){
			return $(s.
				replace(/\(/g, " ( ").
				replace(/\)/g, " ) ").
				split('\n')).
				filter(function(){return this.trim() != ""}).get()};
		var r = clear(reglas), c = clear(consultas);
		var v = [], S = [], R = [];
		$(r.join(' ').split(' ')).each(function () {
			var z = this.trim();
			if(z != "" && $.inArray(z, w) < 0 && $.inArray(z, v) < 0)
				v.push(z);
		});
		var genProps = function(V) {
			var f = [];
			for(var n = 0; n < V.length; n++)
				if(V[n].trim() != "")
					f[n] = eval("(function (" + v.join(", ") + ") { return " +
						(" " + V[n] + " ").
						replace(/([^a-z_])cierto([^a-z_])/g, "$1true$2").
						replace(/([^a-z_])falso([^a-z_])/g, "$1false$2").
						replace(/([^a-z_])no([^a-z_])/g, "$1!$2").
						replace(/([^a-z_])y([^a-z_])/g, "$1&&$2").
						replace(/([^a-z_])o([^a-z_])/g, "$1||$2").
						replace(/([^a-z_])siempre_que([^a-z_])/g, "$1==$2").
						replace(/^(.*)implica_que(.*)$/, "!($1) || ($2)") + " })");
			return f;
		};
		var checkProp = function(f) {return f.apply(window, S)};
		var rF = genProps(r);
		var rC = genProps(c);
		var fail = $(rC).map(function(){return false}).get();
		// todas las combinaciones, cada regla
		for(var s = 0; s <= (1 << v.length); s++) {
			// datos de test
			for(var b = 0; b < v.length; b++)
				S[b] = (s & (1 << b)) != 0;
			// forma parte del conjunto de prueba
			var n = -1;
			while(++n < rF.length)
				if(!checkProp(rF[n]))
					break;
			if(n >= rF.length)
				for(n = 0; n < rC.length; n++)
					if(!fail[n])
						fail[n] = !checkProp(rC[n]);
		}
		// mostramos resultado:
		for(var n = 0; n < rC.length; n++)
			R.push(c[n] + " (ES " + (fail[n] ? "FALSA" : "CIERTA") + ")");
		return R.join("\n");
	}

	function Verificar() {
		$('#resultado').val(MicroVerificador($('#reglas').val(), $('#consultas').val()));
	}
</script>
</head>
<body>
<div>
	<form id="frm">
		Reglas:<br />
<textarea id="reglas" style="width: 100%; height: 250px; color: green">esta_nuboso siempre_que (no llueve y no hace_sol)
llevo_paraguas siempre_que (llueve o hace_sol)
		</textarea><br />
		Consultas:<br />
		<textarea id="consultas" style="width: 100%; height: 100px; color: blue">llevo_paraguas implica_que hace_sol
llevo_paraguas implica_que llueve
		</textarea><br />
		<input type="button" value="Verificar" onclick="Verificar()" /><br />
		Resultados:<br />
		<textarea id="resultado" style="width: 100%; height: 100px; color: purple">
		</textarea>
	</form>
</div>
</body>
</html>
<!--
	La "gramática" admite:

		A siempre_que B		->		A == B
		no A			->		! A
		A y B			->		A && B
		A o B			->		A || B
		A implica_que B		->		! A + B
		( A )


	=========================

	Ejemplo 1:

		Datos:
			esta_nuboso siempre_que (no llueve y no hace_sol)
			llevo_paraguas siempre_que (llueve o hace_sol)

		Pruebas:
			llevo_paraguas implica_que hace_sol
			llevo_paraguas implica_que llueve
			llevo_paraguas implica_que (no esta_nuboso)

	====================================

	Ejemplo 2:

		Datos:
			salgo_vivo siempre_que cierto

			pregunto_mentiroso siempre_que (no salgo_vivo)
			pregunto_sincero siempre_que salgo_vivo

			pregunto_mentiroso_diria_sincero siempre_que (no pregunto_sincero)
			pregunto_sincero_diria_mentiroso siempre_que pregunto_mentiroso

			elijo_contrario_mentiroso_sincero siempre_que (no pregunto_mentiroso_diria_sincero)
			elijo_contrario_sincero_mentiroso siempre_que (no pregunto_sincero_diria_mentiroso)

		Pruebas:
			elijo_contrario_mentiroso_sincero implica_que salgo_vivo
			elijo_contrario_sincero_mentiroso implica_que salgo_vivo

-->
	<!DOCTYPE html>
	<html>
	<head>
	<meta charset="utf-8">
	<title>Micro Verificador de Teoremas</title>
	<script src="http://code.jquery.com/jquery-1.7.2.min.js"></script>
	<script>
	function MicroVerificador(reglas, consultas) {
	var w = ["siempre_que", "no", "y", "o", "implica_que", "cierto", "falso", "(", ")"];
	var clear = function(s){
	return $(s.
	replace(/\(/g, " ( ").
	replace(/\)/g, " ) ").
	split('\n')).
	filter(function(){return this.trim() != ""}).get()};
	var r = clear(reglas), c = clear(consultas);
	var v = [], S = [], R = [];
	$(r.join(' ').split(' ')).each(function () {
	var z = this.trim();
	if(z != "" && $.inArray(z, w) < 0 && $.inArray(z, v) < 0)
	v.push(z);
	});
	var genProps = function(V) {
	var f = [];
	for(var n = 0; n < V.length; n++)
	if(V[n].trim() != "")
	f[n] = eval("(function (" + v.join(", ") + ") { return " +
	(" " + V[n] + " ").
	replace(/([^a-z_])cierto([^a-z_])/g, "$1true$2").
	replace(/([^a-z_])falso([^a-z_])/g, "$1false$2").
	replace(/([^a-z_])no([^a-z_])/g, "$1!$2").
	replace(/([^a-z_])y([^a-z_])/g, "$1&&$2").
	replace(/([^a-z_])o([^a-z_])/g, "$1\|\|$2").
	replace(/([^a-z_])siempre_que([^a-z_])/g, "$1==$2").
	replace(/^(.)implica_que(.)$/, "!($1) \|\| ($2)") + " })");
	return f;
	};
	var checkProp = function(f) {return f.apply(window, S)};
	var rF = genProps(r);
	var rC = genProps(c);
	var fail = $(rC).map(function(){return false}).get();
	// todas las combinaciones, cada regla
	for(var s = 0; s <= (1 << v.length); s++) {
	// datos de test
	for(var b = 0; b < v.length; b++)
	S[b] = (s & (1 << b)) != 0;
	// forma parte del conjunto de prueba
	var n = -1;
	while(++n < rF.length)
	if(!checkProp(rF[n]))
	break;
	if(n >= rF.length)
	for(n = 0; n < rC.length; n++)
	if(!fail[n])
	fail[n] = !checkProp(rC[n]);
	}
	// mostramos resultado:
	for(var n = 0; n < rC.length; n++)
	R.push(c[n] + " (ES " + (fail[n] ? "FALSA" : "CIERTA") + ")");
	return R.join("\n");
	}

	function Verificar() {
	$('#resultado').val(MicroVerificador($('#reglas').val(), $('#consultas').val()));
	}
	</script>
	</head>
	<body>
	<div>
	<form id="frm">
	Reglas:<br />
	<textarea id="reglas" style="width: 100%; height: 250px; color: green">esta_nuboso siempre_que (no llueve y no hace_sol)
	llevo_paraguas siempre_que (llueve o hace_sol)
	</textarea><br />
	Consultas:<br />
	<textarea id="consultas" style="width: 100%; height: 100px; color: blue">llevo_paraguas implica_que hace_sol
	llevo_paraguas implica_que llueve
	</textarea><br />
	<input type="button" value="Verificar" onclick="Verificar()" /><br />
	Resultados:<br />
	<textarea id="resultado" style="width: 100%; height: 100px; color: purple">
	</textarea>
	</form>
	</div>
	</body>
	</html>
	<!--
	La "gramática" admite:

	A siempre_que B -> A == B
	no A -> ! A
	A y B -> A && B
	A o B -> A \|\| B
	A implica_que B -> ! A + B
	( A )


	=========================

	Ejemplo 1:

	Datos:
	esta_nuboso siempre_que (no llueve y no hace_sol)
	llevo_paraguas siempre_que (llueve o hace_sol)

	Pruebas:
	llevo_paraguas implica_que hace_sol
	llevo_paraguas implica_que llueve
	llevo_paraguas implica_que (no esta_nuboso)

	====================================

	Ejemplo 2:

	Datos:
	salgo_vivo siempre_que cierto

	pregunto_mentiroso siempre_que (no salgo_vivo)
	pregunto_sincero siempre_que salgo_vivo

	pregunto_mentiroso_diria_sincero siempre_que (no pregunto_sincero)
	pregunto_sincero_diria_mentiroso siempre_que pregunto_mentiroso

	elijo_contrario_mentiroso_sincero siempre_que (no pregunto_mentiroso_diria_sincero)
	elijo_contrario_sincero_mentiroso siempre_que (no pregunto_sincero_diria_mentiroso)

	Pruebas:
	elijo_contrario_mentiroso_sincero implica_que salgo_vivo
	elijo_contrario_sincero_mentiroso implica_que salgo_vivo

	-->