B. Manual de usuario
Contents
1. Se considerar la siguiente precedencia de operadores Primero las negaciones luego conjun ciones y disyunciones y despu s condicionales y bicondicionales No obstante en caso de duda se aconseja el uso de par ntesis B 1 1 3 Gesti n de par metros En el directorio properties ubicado en el directorio ra z de instalaci n existe un fichero denominado configuration properties en el que se podr n configurar distintos par metros que pos teriormente se mostrar n en los ex menes tipo test generados en formato Tiene especial relevancia la propiedad desordenarFormulas que podr tener dos valores posibles true o false si se actualizase a true despu s de ser cargadas las f rmulas v ase secci n B 1 1 1 durante la ejecuci n de la aplicaci n se proceder a desordenarlas para obtener una mayor aleatoriedad acci n que no ocurrir en caso de estar a false Existen otras dos propiedades tiempoProver9 y tiempoMace4 que servir n para ajustar el tiempo m ximo en segundos en el que Prover9 y Mace4 devuelva una respuesta B 1 2 Ejecuci n del m dulo Para la ejecuci n de este m dulo podr utilizar algunos de los ficheros ubicados en el directorio ra z de instalaci n gen Test bat Windows o Test sh Linux su sintaxis ser la siguiente B 2 M dulo evaluador 123 Gen Test t f file zml g n l p hfelp B 1 2 1 Generaci n de ficheros con datos preprocesados La principal2. Manual de usuario B 1 M dulo generador Este m dulo se ejecutar en el ordenador personal del profesor pudiendo realizar las siguientes acciones Generar ficheros con datos preprocesados que posteriormente ser n exportados al entorno de evaluaci n de conocimientos SIETT T E Generar ex menes tipo test en formato IATEX Probar la correcta instalaci n de componentes Adem s se podr n configurar distintas opciones as como agregar nuevas f rmulas proposicionales y de primer orden seg n estime el equipo docente B 1 1 Opciones de configuraci n Una vez instalado el m dulo generador en el ordenador personal del profesor y antes de ejecutar la aplicaci n se debe tener en cuenta la posibilidad de configurar distintas opciones as como agregar o eliminar f rmulas proposicionales y de primer orden que la aplicaci n tendr en cuenta a la hora de realizar los c lculos B 1 1 1 Gesti n de f rmulas En el directorio Formulas ubicado en el directorio ra z de instalaci n existen dos ficheros propositional txt y firstOrder txt que contienen las f rmulas proposicionales y de primer orden a partir de las cu les la aplicaci n realiza los c lculos Para dar mayor flexibilidad se permite mediante cualquier editor de textos que el usuario agregue elimine o comente aquellas que estime oportunas teniendo en cuenta las siguientes premisas En el fichero propositional txt se gestionar n las f
3. a Solo Yi b a AY y Y c nia Y nia Y gt 23 La interpretaci n 1 satisface a Solo Yi b a AY y Y c nia Y nia Y Datos L gica Proposicional EV q gt p Xo PAqQ gt rVs pva gt rAs L gica de Predicados Yo VaVy gt dz A Qzy VaVy dz Quz V Interpretaciones dominio U 0 1 con S 0 0 0 1 If dominio U 0 1 con S 0 Q 90 Ii dominio U 0 1 con Q 0 1 S 0 0 0 1 137
4. rmulas proposicionales mientras que en firstOrder txt las de primer orden S lo podr haber una f rmula por l nea Se pueden comentar las f rmulas anteponiendo la cadena Las f rmulas comentadas no se tratar n durante la ejecuci n 121 122 Capitulo B Manual de usuario Operador y Cuantificadores Ejemplo Prover9 Negaci n Disyunci n V Conjunci n A amp p amp q gt Bicondicional gt p lt gt q Existe 3 exists exists x exists y Para todo V Tabla B 1 Manual de usuario Sintaxis formulas Condicional gt p gt a La sintaxis utilizada ser la propuesta por Prover9 v ase secci n B 1 1 2 B 1 1 2 Sintaxis f rmulas La sintaxis de las f rmulas almacenadas en los ficheros propositional txt y firstOrder txt es la propuesta por Prover9 En general existe una regla para distinguir variables de constantes Por defecto una variable empezara por una letra minuscula comprendida entre la u y la z considerandose constantes el resto de letras Por ejemplo en la f rmula P a x el t rmino a es una constante y x es una variable Los operadores y cuantificadores utilizados son los siguientes Con car cter general tanto las relaciones como las funciones utilizadas en las f rmulas de predicados de primer orden se incluir n entre par ntesis y separados por comas sus constantes y variables por ejemplo VxWyPxy se representar a en Prover9 como all x all y P x y
5. qorVs 8 Indique la formula no equivalente a X a t gt a V p b ct a V p c p qorVs 9 El conjunto satisfacible es a LY Y b Yo Y3 c Yo Y3 10 El conjunto insatisfacible es Y Y3 b AR Y2 13 c Yd Yo 11 12 13 14 15 16 Senale la tautologia b Y gt Yj Y Senale cual no es tautologia Ya b Y gt e tX Y La consecuencia correcta es a lY Y2 E 7Y3 b Y1 Y E Ys c Y Yo Ys La consecuencia no correcta es a lY Y2 E Ya b 14 0 pow c Y Yo Y Indique la f rmula equivalente a Yj VaVy gt dz Qxz Qzy b AarVySay c dxdy S zy Indique la f rmula no equivalente a Yi AaVySay b dx Ayas zry ex Glar 135 186 Cap tulo C Ejemplo de test generado de forma autom tica 17 Sobre el Universo U 0 1 Qu interpretaci n satisface Y Yo Y37 S 0Q 0 es insatisfacible 18 Sobre el Universo U 0 1 Qu interpretaci n satisface Y Yo Y3 Q 0 5 4 b Q 0 5 0 0 0 1 c es insatisfacible 19 La interpretacion 1 no satisface a Ya b AY c Yo 20 La interpretaci n 13 satisface a Yo b Y c 21 La interpretaci n I1 satisface a Solo Y2 b a Ya y Y c nia Yo nia Y 22 La interpretaci n 12 satisface
6. un fichero con datos preprocesados gen erado previamente crear un fichero con un examen tipo test en formato IATEX En ambos casos los ficheros generados se depositar n en el directorio LaTexTests ubicado en el directorio ra z de instalaci n B 1 2 3 Otras opciones Adem s de los modificadores descritos anteriormente existen otros dos a tener encuentra GenTest p Permitir comprobar que todos los componentes necesarios tales como Prover9 y Mace4 est n instalados correctamente GenTest h Mostrar una ayuda con una descripci n de uso de los distintos modificadores B 2 M dulo evaluador Antes de utilizar las instrucciones mostradas a continuaci n se supone que el profesor tiene una cuenta en SIET T E con derechos de administraci n sobre la asignatura L gica Computacional 124 Capitulo B Manual de usuario B 2 1 Configuraci n de la asignatura En primer lugar deber configurar los par metros de la asignatura El profesor acceder a SIETTE acredit ndose con su usuario y contrase a Se acceder a la opci n Editar asignatura IO Ediarasignaira nn Clic sobre la asignatura lgebra Computacional 8 Algebra Computacional continuaci n transferir todos los ficheros XML con datos preprocesados creados con el m dulo generador v ase A 1 mediante el panel Gesti n de Archivos una vez seleccionado el directorio ac LogicExam Gesti n de archivos Directorio
7. ac LogicExams Eliminar Nuevo directorio LogicExam0000 xml LogicExam0001 xml LogicExam0002 xml LogicExam0003 xml LogicExam0004 xml Enviar fichero Figura B 1 Manual Usuario Gesti n de archivos preprocesados Aseg rese que en el panel Datos de la Asignatura la opci n Utilizar f rmulas MathJax est a Si Id 5309 ID tema inicial 20127 Nombre Algebra Computacional N mero de niveles de conocimiento 12 Editor Hermes v Utilizar f rmulas MathJax Si O No Figura B 2 Manual Usuario SIETTE Configuraci n de MathJax Aunque se han preconfigurado dos temas L gica de proposiciones y L gica de predicados de primer orden B 2 M dulo evaluador 125 rsen Algebra Computacional 5 88 L gica de predicados L gica de Proposiciones L gica de predicados de primer orden Figura B 3 Manual Usuario SIETTE Temas preconfigurados puede agregar los temas que considere oportunos con la opci n Nuevo gt Tema Nuevo tema Figura B 4 Manual Usuario SIETTE Nuevo tema B 2 2 Creaci n de preguntas Para crear preguntas siga los siguientes pasos Si necesita crear una pregunta sin tener ninguna otra como referencia seleccione el tema de la pregunta bee Algebra Computacional 2 93 L gica de predicados t L gica de predicados de primer orden Figura B 5 Manual Usuario SIETTE Selecci n tema Seleccione la opci n Nu
8. est En la Descripci n es aconsejable escribir el siguiente texto aclaratorio en formato HTML B font size 4 gt lt B gt jAVISO lt B gt lt font gt lt B gt lt br gt lt br gt Tenga en cuenta que en cada pregunta se le presentar un bot n de ayuda lt B gt Ayuda 1 x 1 0 B al ser pulsada se le mostrar n conceptos generales te ricos respecto a la pregunta en curso br br Al finalizar el test le mostrar una soluci n detallada tanto de las respuestas correctas como incorrectas En el n mero de preguntas el criterio de selecci n as como los temas podr n variar seg n las preferencias del profesor C Ejemplo de test generado de for ma autom tica 1 El conjunto satisfacible es a Xi X3 b AX1 5X2 e AX 1 AX 3 2 El conjunto insatisfacible es a Xi b AX1 X2 7X3 c aXe aX 3 3 Senale la tautologia 1 b LX X c X 7 4 Senale cual es tautologia Xy X gt Xa b X E c Xi A X 188 184 Cap tulo C Ejemplo de test generado de forma autom tica 5 La consecuencia correcta es a 2X3 X2 F b 1X1 X E c X1 7X2 E 6 La consecuencia no correcta es a 2X3 2X2 F 7X3 0 7X1 X2 E c X1 7X2 Indique la formula equivalente a X4 pPVI gt TAS 0 ot gt a V p c p
9. evo gt Pregunta TL oem Nuevo pregunta gt Ak Figura B 6 Manual Usuario SIETTE Nueva pregunta Seleccione el tipo Opci n M ltiple Respuesta nica Figura B 7 Manual Usuario SIETTE Pregunta opci n m ltiple 126 Capitulo B Manual de usuario En la pregunta que est configurando escriba el enunciado el siguiente c digo JSP lt page language java contentType text html charset UTF 8 pageEncoding UTF 8 lt A page import es uned genTest view lt PreguntaLogica preguntaLogica new ProposicionalSatisfacible ac LogicExams Random nextLong String enunciado preguntaLogica getEnunciado String respuestaCorrecta preguntaLogica getRespuestaCorrecta String respuestalncorrectal preguntaLogica getRespuestasIncorrectas get 0 String respuestalncorrecta2 preguntaLogica getRespuestasIncorrectas get 1 String ayudaRespuestaCorrecta preguntaLogica getSolucionCorrecta String ayudaRespuestalncorrectal preguntaLogica getSolucionesInCorrectas get 0 String ayudaRespuestalncorrecta2 preguntaLogica getSolucionesInCorrectas get 1 String conceptosGenerales preguntaLogica getConceptosGenerales lt enunciado A continuaci n agregue las respuestas tal y como se muestra en la figura respusestacorr amp ecta A Eliminar Editar Es comecta f respuaestaInsorrectal br Modificar lt h respuesrzai
10. finalidad de este m dulo es la obtenci n de ficheros con datos preprocesados en formato XML que posteriormente ser n exportados al entorno de evaluaci n de conocimientos SIETTE v ase secci n B 2 1 Para este fin se dispone de dos modificadores GenTest g Generar un fichero XML con datos preprocesados configurado para desplegar en GenTest g n Generar n ficheros XML con datos preprocesados configurado para desple gar en SIETTE Por ejemplo si se ejecuta Gen Test g 3 se generar n tres ficheros XML con datos preprocesados En ambos casos los ficheros generados se depositar n en el directorio LogicTestsX ML ubicado en el directorio ra z de instalaci n B 1 2 2 Generaci n de ex menes tipo test en formato Como finalidad opcional de este m dulo se podr n generar ex menes tipo test en formato IATEX Para este fin se dispone de dos modificadores GenTest t Generar un examen en formato incluyendo en los datos comunes cuatro f rmulas proposicionales y cuatro de primer orden GenTest t f file xml Generar un examen en formato IATEX tomando como referen cia el fichero xml este fichero corresponder a un fichero XML con datos preprocesados generado previamente El examen resultante contendr en sus datos comunes tres f rmu las proposicionales y tres f rmulas de primer orden Por ejemplo si se ejecuta GenTest t fF LogicExam0000 xml donde LogicExam0000 xml es
11. ncorrecraz Modifica Eliminar Es correcta Figura B 8 Manual Usuario SIETTE Agregar respuestas B 2 M dulo evaluador 127 Para agregar el refuerzo a la respuesta correcta para ello pulse el bot n Modificar ubicado a la derecha de lt respuestaCorrecta gt y rellene la de Refuerzo con el siguiente texto lt ayudaRespuestaCorrecta lt br gt lt br gt Pero le interesar amp aacute saber que lt br gt lt br gt lt ayudaRespuestalncorrectal lt br gt lt br gt y adem amp aacute s lt br gt lt br gt lt ayudaRespuestalncorrecta2 Por tanto el refuerzo quedar configurado tal y como se muestra en la figura Despuestelorrecta gt q amp ayudaBespusestACOIIeCcLtA Xoxbrs bDr Pero le interesarL amp ACuLe saber que lt brs lt bis lt amp ayudaBespuestAIlncorrecrtaAl y amp d ZLARCuL amp IBI XDIISIDI lt AyudAReSpuesztAIDncOrr amp ctAZ gt Cenar Figura B 9 Manual Usuario SIETTE Refuerzo respuesta correcta A continuaci n pulse el bot n Cerrar Para agregar el refuerzo a las respuestas incorrectas pulse el bot n Modificar ubicado a la derecha de lt respuestalncorrectal gt y lt respuestalncorrecta2 gt respectiva mente y rellene la caja de Refuerzo con el siguiente texto en el caso de la respuesta incorrecta 2 sustituya ayudaRespuestalncorrectal por ayudaRespuestalncorrecta2 lt ayudaRespuestalnc
12. orrectal x lt br gt lt br gt Sin embargo puede constatar que lt br gt lt br gt lt ayudaRespuestaCorrecta lt br gt lt br gt 128 Capitulo B Manual de usuario Por tanto el refuerzo quedara configurado tal y como se muestra en la figura recuerde realizar la misma acci n para la respuesta incorrecta 2 respuestalncorrecral b gt ayudafespuestalncorrectal Az brz br Sin embargo puede constatar que cbrzscbr qia ayudaRespu estazorrecta gt gt Figura B 10 Manual Usuario SIETTE Refuerzo respuestas incorrectas A continuaci n pulse el bot n Cerrar Configure la opci n de refuerzo lt conceptosGenerales gt Refuerzo cuando el alumno no d ninguna respuesta Figura B 11 Manual Usuario SIETTE Refuerzo conceptos generales Y las ayuda Ayuda Che conceptosGenerales i Figura B 12 Manual Usuario SIETTE Ayuda conceptos generales Finalmente Guarde Cambios B 2 M dulo evaluador 129 En el panel Previsualizar puede comprobar como lo ver el alumno 01 Grupo Formulas Satisfacibles Dadas las siguientes f rmulas proposicionales el conjunto satisfacible es Xi Ee 74 gt p X3 v rvs 3 pAqrrvs X1 7X2 X3 X1 X2 X3 O X1 X2 7X3 l Guardar cambios Eliminar Duplicar pregunta Figura B 13 Manual Usuario SIETTE Previsualizaci n de preguntas A partir de esta pregunta generar otras
13. preguntas es sumamente sencillo lo nico que deber hacer es seleccionar el bot n Duplicar Pregunta Guardar cambios Eliminar Duplicar pregunta Figura B 14 Manual Usuario SIETTE Duplicar pregunta 180 Capitulo B Manual de usuario y sustituir en el enunciado el modelo de pregunta tiene veintitr s modelos disponibles es de Cir en PreguntaLogica preguntaLogica new ProposicionalSatisfacible ac LogicExams Random nextLong sustituir ProposicionalSatisfacible por otro de los mostrados a en la tabla adjunta se detalla cada modelo con una pregunta de ejemplo que podr consultar en pendice C 7 Numero de Pregunta Modelo de Pregunta ProposicionalSatisfacible ProposciomalnSaishble 2 3 ProposicionalNoTamtologia 1 ProposicionalConsecnencia ProposicionalNoConsecuencia ProposicionalNoEquivalentes oo o sS PredicadoSatisfacible Prdiadohatsadble 0 PrdicdoNoComecwnda PredicadoEquivalentes PredicadoNoEquivalentes PredicadolnterpretacionSatisfacible PredicadolnterpretacionNoSatisfaceFormala 19 PredicadolnterpretacionSatisfaceFormala 20 PredicadolnterpretacionSatisfacibleFormulaSoloUna 21 Tabla B 2 Manual de usuario Modelos de preguntas disponibles La cadena ac Logickxams indica que se elija al azar un fichero de datos preprocesado pero si el profesor lo estima oportuno puede
14. seleccionar uno en concreto por ejemplo para forzar que se utilice el fichero LogicExam0000 xml se escribir a PreguntaLogica preguntaLogica new ProposicionalSatisfacible ac LogicExams LogicExam0000 xml Random nextLong B 2 M dulo evaluador 181 B 2 3 Creaci n de ex menes tipo test continuaci n bas ndose en las preguntas creadas en el punto anterior el profesor podr configurar los ex menes tipo test que crea oportunos para ello siga los siguientes pasos Seleccione bot n Tests Figura B 15 Manual Usuario SIETTE Boton Tests Seleccione bot n Nuevo Test Nuevo test Figura B 16 Manual Usuario SIETTE Bot n Nuevo Test Cumplimente el panel de Informaci n tal y como se muestra en la figura Id 14607 URL http www siette org 80 siette idtest 14607 Titulo Algebra Computacional incluye algebra proposiciona Tenga en cuenta que en cada pregunta se le Descripci n presentar un bot n de ayuda lt B gt Ayuda 1 x 1 0 lt B gt al ser pulsada se le mostrar n conceptos generales te ricos respecto a la pregunta en curso lt br gt lt br gt Fecha de creaci n 2012 02 06 15 59 04 Autor Joaquin Campillo Molina ltima modificaci n 2012 2 8 22 52 23 Autor de la modificaci n Joaquin Campillo Molina Activo e S O No Guardar cambios l Eliminar Duplicar test Probar Figura B 17 Manual Usuario Panel de Informaci n del t
Download Pdf Manuals
Related Search